From d338b17788aef185ffc58df3db4baf8666e10b5a Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Thu, 25 Jan 2024 16:06:51 +0100
Subject: [PATCH 1/5] added $j tags, *ALT -> *g, updated changes-set.txt

---
 changes-set.txt |  44 ++++++++++++++++++++-
 discouraged     |  11 ------
 set.mm          | 100 ++++++++++++++++++++++++++++--------------------
 3 files changed, 102 insertions(+), 53 deletions(-)

diff --git a/changes-set.txt b/changes-set.txt
index 60304da5e6..f8c44553e3 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -14,6 +14,44 @@ The ones WITH "Notes" may have to be processed manually.
 
 PROPOSED:
 Date      Old       New         Notes
+proposed  nfiundg   nfiund
+proposed  bnj1441g  bnj1441
+proposed  cbviinvg  cbviinv
+proposed  cbviunvg  cbviunv
+proposed  cbviing   cbviin
+proposed  cbviung   cbviun
+proposed  nfiing    nfiin
+proposed  nfiung    nfiun
+proposed  nfrexg    nfrex
+proposed  nfrexdg   nfrexd
+proposed  nfaba1g   nfaba1
+proposed  nfabg     nfab
+proposed  hblemg    hblem
+proposed  nfsabg    nfsab
+proposed  hbabg     hbab
+proposed  cbvmptvg  cbvmptv
+proposed  cbvmptg   cbvmpt
+proposed  cbvmptfg  cbvmptf
+proposed  cbvopab1g cbvopab1
+proposed  nfiund    nfiundv
+proposed  bnj1441   bnj1441v
+proposed  cbviinv   cbviinvv
+proposed  cbviunv   cbviunvv
+proposed  cbviin    cbviinv
+proposed  cbviun    cbviunv
+proposed  nfiin     nfiinv
+proposed  nfiun     nfiunv
+proposed  nfrex     nfrexv
+proposed  nfrexd    nfrexdv
+proposed  nfaba1    nfaba1v
+proposed  nfab      nfabv
+proposed  hblem     hblemv
+proposed  nfsab     nfsabv
+proposed  hbab      hbabv
+proposed  cbvmptv   cbvmptvv
+proposed  cbvmpt    cbvmptv
+proposed  cbvmptf   cbvmptfv
+proposed  cbvopab1  cbvopab1v
 proposed  syl       imtri       (analogous to *bitr*, sstri, etc.)
                                 there is less agreement on renaming syl
                                 than others here
@@ -94,7 +132,11 @@ Date      Old       New         Notes
 20-Jan-24 nfab      nfabg
 20-Jan-24 hblem     hblemg
 20-Jan-24 nfsab     nfsabg
-20-Jan-24 hbab      hbabg 
+20-Jan-24 hbab      hbabg
+17-Jan-24 cbvmptv   cbvmptvg
+17-Jan-24 cbvmpt    cbvmptg
+17-Jan-24 cbvmptf   cbvmptfg
+17-Jan-24 cbvopab1  cbvopab1g
 17-Jan-24 mteqand   [same]      moved from SN's mathbox to main set.mm
 15-Jan-24 sseqtr4d  sseqtrrd
 14-Jan-24 sseqtr4i  sseqtrri
diff --git a/discouraged b/discouraged
index e5af1f2e2b..50ba3d858a 100755
--- a/discouraged
+++ b/discouraged
@@ -2998,9 +2998,6 @@
 "cbncms" is used by "ubthlem2".
 "cbvexsv" is used by "onfrALTlem1".
 "cbvexsv" is used by "onfrALTlem1VD".
-"cbvmptALT" is used by "cbvmptvALT".
-"cbvmptfALT" is used by "cbvmptALT".
-"cbvopab1ALT" is used by "cbvmptfALT".
 "cdj3lem1" is used by "cdj3i".
 "cdj3lem1" is used by "cdj3lem2b".
 "cdj3lem2" is used by "cdj3i".
@@ -14063,10 +14060,6 @@ New usage of "cbvalvOLD" is discouraged (0 uses).
 New usage of "cbveuALT" is discouraged (0 uses).
 New usage of "cbvexsv" is discouraged (2 uses).
 New usage of "cbvexvOLD" is discouraged (0 uses).
-New usage of "cbvmptALT" is discouraged (1 uses).
-New usage of "cbvmptfALT" is discouraged (1 uses).
-New usage of "cbvmptvALT" is discouraged (0 uses).
-New usage of "cbvopab1ALT" is discouraged (1 uses).
 New usage of "cbvrabvOLD" is discouraged (0 uses).
 New usage of "cbvrexdva2OLD" is discouraged (0 uses).
 New usage of "ccat2s1fvwALT" is discouraged (0 uses).
@@ -18219,10 +18212,6 @@ Proof modification of "cbvalvOLD" is discouraged (53 steps).
 Proof modification of "cbveuALT" is discouraged (48 steps).
 Proof modification of "cbvexsv" is discouraged (29 steps).
 Proof modification of "cbvexvOLD" is discouraged (38 steps).
-Proof modification of "cbvmptALT" is discouraged (15 steps).
-Proof modification of "cbvmptfALT" is discouraged (166 steps).
-Proof modification of "cbvmptvALT" is discouraged (13 steps).
-Proof modification of "cbvopab1ALT" is discouraged (187 steps).
 Proof modification of "cbvrabvOLD" is discouraged (19 steps).
 Proof modification of "cbvrexdva2OLD" is discouraged (128 steps).
 Proof modification of "ccat2s1fvwALT" is discouraged (149 steps).
diff --git a/set.mm b/set.mm
index 6a8e670435..b1c9b3dfa7 100644
--- a/set.mm
+++ b/set.mm
@@ -25097,6 +25097,7 @@ yield an eliminable and weakly (that is, object-level) conservative
        (Revised by Gino Giotto, 20-Jan-2024.) $)
     hbab $p |- ( z e. { y | ph } -> A. x z e. { y | ph } ) $=
       ( cv cab wcel wsb df-clab hbsbw hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
+    $( $j usage 'hbab' avoids 'ax-13'; $)
   $}
 
   ${
@@ -25117,6 +25118,7 @@ yield an eliminable and weakly (that is, object-level) conservative
        more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfsab $p |- F/ x z e. { y | ph } $=
       ( cv cab wcel nf5ri hbab nf5i ) DFACGHBABCDABEIJK $.
+    $( $j usage 'nfsab' avoids 'ax-13'; $)
   $}
 
   ${
@@ -27075,6 +27077,7 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
        more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfab $p |- F/_ x { y | ph } $=
       ( vz cab nfsab nfci ) BEACFABCEDGH $.
+    $( $j usage 'nfab' avoids 'ax-13'; $)
   $}
 
   ${
@@ -27094,6 +27097,7 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
        more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfaba1 $p |- F/_ x { y | A. x ph } $=
       ( wal nfa1 nfab ) ABDBCABEF $.
+    $( $j usage 'nfaba1' avoids 'ax-13'; $)
   $}
 
   $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
@@ -29810,6 +29814,7 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     nfrexd $p |- ( ph -> F/ x E. y e. A ps ) $=
       ( wrex wn wral dfrex2 nfnd nfraldw nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGA
       BCHMNMO $.
+    $( $j usage 'nfrexd' avoids 'ax-13'; $)
   $}
 
   ${
@@ -29836,6 +29841,7 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     nfrex $p |- F/ x E. y e. A ph $=
       ( wrex wnf wtru nftru wnfc a1i nfrexd mptru ) ACDGBHIABCDCJBDKIELABHIFLMN
       $.
+    $( $j usage 'nfrex' avoids 'ax-13'; $)
   $}
 
   ${
@@ -44842,6 +44848,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     nfiun $p |- F/_ y U_ x e. A B $=
       ( vz ciun cv wcel wrex cab df-iun nfcri nfrex nfab nfcxfr ) BACDHGIDJZACK
       ZGLAGCDMSBGRBACEBGDFNOPQ $.
+    $( $j usage 'nfiun' avoids 'ax-13'; $)
 
     $( Bound-variable hypothesis builder for indexed intersection.
        (Contributed by Mario Carneiro, 25-Jan-2014.)  Add disjoint variable
@@ -44851,6 +44858,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     nfiin $p |- F/_ y |^|_ x e. A B $=
       ( vz ciin cv wcel wral cab df-iin nfcri nfralw nfab nfcxfr ) BACDHGIDJZAC
       KZGLAGCDMSBGRBACEBGDFNOPQ $.
+    $( $j usage 'nfiin' avoids 'ax-13'; $)
   $}
 
   ${
@@ -44971,6 +44979,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
       ( vz cv wcel wrex cab ciun nfcri weq eleq2d cbvrexw abbii df-iun 3eqtr4i
       ) IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBI
       CETUA $.
+    $( $j usage 'cbviun' avoids 'ax-13'; $)
 
     $( Change bound variables in an indexed intersection.  (Contributed by Jeff
        Hankins, 26-Aug-2009.)  (Revised by Mario Carneiro, 14-Oct-2016.)  Add
@@ -44981,6 +44990,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
       ( vz cv wcel wral cab ciin nfcri weq eleq2d cbvralw abbii df-iin 3eqtr4i
       ) IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBI
       CETUA $.
+    $( $j usage 'cbviin' avoids 'ax-13'; $)
   $}
 
   ${
@@ -45014,6 +45024,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
        (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
+    $( $j usage 'cbviunv' avoids 'ax-13'; $)
 
     $( Change bound variables in an indexed intersection.  (Contributed by Jeff
        Hankins, 26-Aug-2009.)  Add disjoint variable condition to avoid
@@ -45021,6 +45032,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
        axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviinv $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( nfcv cbviin ) ABCDEBDGAEGFH $.
+    $( $j usage 'cbviinv' avoids 'ax-13'; $)
   $}
 
   ${
@@ -46705,18 +46717,18 @@ although the definition does not require it (see ~ dfid2 for a case
       CJUAZNZDOZJOVHVAVNCJVAJRVMCDVKVLCVKCRACJUBSTUPVIMZUTVMDVOUSVKAVLVOURVJUOU
       PVIUQUCUDACJUEUFUGUHVNVGJEVMEDVKVLEVKERACJEFUISTVGJRVIVCMZVMVFDVPVKVEVLBV
       PVJVDUOVIVCUQUCUDABCJVCGHUJUFUGUHUKULACDIUMBEDIUMUN $.
+    $( $j usage 'cbvopab1' avoids 'ax-13'; $)
   $}
 
   ${
     $d v w x y $.  $d v w y z $.  $d v w ph $.  $d v w ps $.
-    cbvopab1ALT.1 $e |- F/ z ph $.
-    cbvopab1ALT.2 $e |- F/ x ps $.
-    cbvopab1ALT.3 $e |- ( x = z -> ( ph <-> ps ) ) $.
-    $( Alternate version of ~ cbvopab1 , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 6-Oct-2004.)  (Revised by Mario Carneiro,
-       14-Oct-2016.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cbvopab1ALT $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
+    cbvopab1g.1 $e |- F/ z ph $.
+    cbvopab1g.2 $e |- F/ x ps $.
+    cbvopab1g.3 $e |- ( x = z -> ( ph <-> ps ) ) $.
+    $( Change first bound variable in an ordered-pair class abstraction, using
+       explicit substitution.  (Contributed by NM, 6-Oct-2004.)  (Revised by
+       Mario Carneiro, 14-Oct-2016.) $)
+    cbvopab1g $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
       ( vw vv cv cop wceq wa wex cab copab wsb nfv nfan nfs1v nfex opeq1 eqeq2d
       sbequ12 anbi12d exbidv cbvexv1 nfsb sbequ sbie syl6bb bitri abbii df-opab
       3eqtr4i ) IKZCKZDKZLZMZANZDOZCOZIPUQEKZUSLZMZBNZDOZEOZIPACDQBEDQVDVJIVDUQ
@@ -46982,7 +46994,9 @@ although the definition does not require it (see ~ dfid2 for a case
        substitution.  This version has bound-variable hypotheses in place of
        distinct variable conditions.  (Contributed by NM, 11-Sep-2011.)
        (Revised by Thierry Arnoux, 9-Mar-2017.)  Add disjoint variable
-       condition to avoid ~ ax-13 .  (Revised by Gino Giotto, 17-Jan-2024.) $)
+       condition to avoid ~ ax-13 .  See ~ cbvmptfg for a less restrictive
+       version requiring more axioms.  (Revised by Gino Giotto,
+       17-Jan-2024.) $)
     cbvmptf $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( vz vw cv wcel wceq wa copab cmpt wsb weq nfv nfcri nfs1v eleq1w sbequ12
       nfan anbi12d cbvopab1 nfeq2 nfsbv sbequ eqeq2d sbiev syl6bb eqtri 3eqtr4i
@@ -46990,26 +47004,27 @@ although the definition does not require it (see ~ dfid2 for a case
       IAKLVALUAVGVHAALCFUBUTALUCUFALTURVGUTVHALCUDUTALUEUGUHVIVELKBVGVHBBLCGUBU
       TALBBUSDHUIUJUFVELUALBTZVGVCVHVDLBCUDVJVHUTABSVDUTLBAUKUTVDABAUSEIUIABTDE
       USJULUMUNUGUHUOAKCDUQBKCEUQUP $.
+    $( $j usage 'cbvmptf' avoids 'ax-13'; $)
   $}
 
   ${
     $d w z x $.  $d w z y $.  $d w z A $.  $d w z B $.  $d w z C $.
-    cbvmptfALT.1 $e |- F/_ x A $.
-    cbvmptfALT.2 $e |- F/_ y A $.
-    cbvmptfALT.3 $e |- F/_ y B $.
-    cbvmptfALT.4 $e |- F/_ x C $.
-    cbvmptfALT.5 $e |- ( x = y -> B = C ) $.
-    $( Alternate version of ~ cbvmptf , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 11-Sep-2011.)  (Revised by Thierry
-       Arnoux, 9-Mar-2017.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cbvmptfALT $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
+    cbvmptfg.1 $e |- F/_ x A $.
+    cbvmptfg.2 $e |- F/_ y A $.
+    cbvmptfg.3 $e |- F/_ y B $.
+    cbvmptfg.4 $e |- F/_ x C $.
+    cbvmptfg.5 $e |- ( x = y -> B = C ) $.
+    $( Rule to change the bound variable in a maps-to function, using implicit
+       substitution.  This version has bound-variable hypotheses in place of
+       distinct variable conditions.  (Contributed by NM, 11-Sep-2011.)
+       (Revised by Thierry Arnoux, 9-Mar-2017.) $)
+    cbvmptfg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( vz vw cv wcel wceq wa copab cmpt wsb weq nfv nfcri nfs1v eleq1w sbequ12
-      nfan anbi12d cbvopab1ALT nfeq2 nfsb sbequ eqeq2d sbie syl6bb eqtri df-mpt
-      3eqtr4i ) AMCNZKMZDOZPZAKQZBMCNZUSEOZPZBKQZACDRBCERVBLMCNZUTALSZPZLKQVFVA
-      VIAKLVALUAVGVHAALCFUBUTALUCUFALTURVGUTVHALCUDUTALUEUGUHVIVELKBVGVHBBLCGUB
-      UTALBBUSDHUIUJUFVELUALBTZVGVCVHVDLBCUDVJVHUTABSVDUTLBAUKUTVDABAUSEIUIABTD
-      EUSJULUMUNUGUHUOAKCDUPBKCEUPUQ $.
+      nfan anbi12d cbvopab1g nfeq2 nfsb sbequ eqeq2d sbie syl6bb df-mpt 3eqtr4i
+      eqtri ) AMCNZKMZDOZPZAKQZBMCNZUSEOZPZBKQZACDRBCERVBLMCNZUTALSZPZLKQVFVAVI
+      AKLVALUAVGVHAALCFUBUTALUCUFALTURVGUTVHALCUDUTALUEUGUHVIVELKBVGVHBBLCGUBUT
+      ALBBUSDHUIUJUFVELUALBTZVGVCVHVDLBCUDVJVHUTABSVDUTLBAUKUTVDABAUSEIUIABTDEU
+      SJULUMUNUGUHUQAKCDUOBKCEUOUP $.
   $}
 
   ${
@@ -47020,22 +47035,24 @@ although the definition does not require it (see ~ dfid2 for a case
     $( Rule to change the bound variable in a maps-to function, using implicit
        substitution.  This version has bound-variable hypotheses in place of
        distinct variable conditions.  (Contributed by NM, 11-Sep-2011.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       disjoint variable condition to avoid ~ ax-13 .  See ~ cbvmptg for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
        17-Jan-2024.) $)
     cbvmpt $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( nfcv cbvmptf ) ABCDEACIBCIFGHJ $.
+    $( $j usage 'cbvmpt' avoids 'ax-13'; $)
   $}
 
   ${
     $d w z x A $.  $d w z y A $.  $d w z B $.  $d w z C $.
-    cbvmptALT.1 $e |- F/_ y B $.
-    cbvmptALT.2 $e |- F/_ x C $.
-    cbvmptALT.3 $e |- ( x = y -> B = C ) $.
-    $( Alternate version of ~ cbvmpt , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 11-Sep-2011.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    cbvmptALT $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
-      ( nfcv cbvmptfALT ) ABCDEACIBCIFGHJ $.
+    cbvmptg.1 $e |- F/_ y B $.
+    cbvmptg.2 $e |- F/_ x C $.
+    cbvmptg.3 $e |- ( x = y -> B = C ) $.
+    $( Rule to change the bound variable in a maps-to function, using implicit
+       substitution.  This version has bound-variable hypotheses in place of
+       distinct variable conditions.  (Contributed by NM, 11-Sep-2011.) $)
+    cbvmptg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
+      ( nfcv cbvmptfg ) ABCDEACIBCIFGHJ $.
   $}
 
   ${
@@ -47043,20 +47060,21 @@ although the definition does not require it (see ~ dfid2 for a case
     cbvmptv.1 $e |- ( x = y -> B = C ) $.
     $( Rule to change the bound variable in a maps-to function, using implicit
        substitution.  (Contributed by Mario Carneiro, 19-Feb-2013.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
-       17-Jan-2024.) $)
+       disjoint variable condition to avoid ~ ax-13 .  See ~ cbvmptvg for a
+       less restrictive version requiring more axioms.  (Revised by Gino
+       Giotto, 17-Jan-2024.) $)
     cbvmptv $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( nfcv cbvmpt ) ABCDEBDGAEGFH $.
+    $( $j usage 'cbvmptv' avoids 'ax-13'; $)
   $}
 
   ${
     $d A x $.  $d A y $.  $d B y $.  $d C x $.
-    cbvmptvALT.1 $e |- ( x = y -> B = C ) $.
-    $( Alternate version of ~ cbvmptv , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 19-Feb-2013.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    cbvmptvALT $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
-      ( nfcv cbvmptALT ) ABCDEBDGAEGFH $.
+    cbvmptvg.1 $e |- ( x = y -> B = C ) $.
+    $( Rule to change the bound variable in a maps-to function, using implicit
+       substitution.  (Contributed by Mario Carneiro, 19-Feb-2013.) $)
+    cbvmptvg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
+      ( nfcv cbvmptg ) ABCDEBDGAEGFH $.
   $}
 
   ${

From 1fb94b90c5ba23e1e52991aee7955b5eca3be3be Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Thu, 25 Jan 2024 16:24:12 +0100
Subject: [PATCH 2/5] comment update

---
 set.mm | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/set.mm b/set.mm
index b1c9b3dfa7..5823477e62 100644
--- a/set.mm
+++ b/set.mm
@@ -46709,7 +46709,8 @@ although the definition does not require it (see ~ dfid2 for a case
     $( Change first bound variable in an ordered-pair class abstraction, using
        explicit substitution.  (Contributed by NM, 6-Oct-2004.)  (Revised by
        Mario Carneiro, 14-Oct-2016.)  Add disjoint variable condition to avoid
-       ~ ax-13 .  (Revised by Gino Giotto, 17-Jan-2024.) $)
+       ~ ax-13 .  See ~ cbvopab1g for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 17-Jan-2024.) $)
     cbvopab1 $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
       ( vw vv cv cop wceq wa wex cab copab nfv nfan nfex wsb nfs1v opeq1 eqeq2d
       sbequ12 anbi12d exbidv cbvexv1 nfsbv sbhypf bitri abbii df-opab 3eqtr4i )

From 53817b98836f6686b9b989907ae7aef83409bee3 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 27 Jan 2024 12:51:15 +0100
Subject: [PATCH 3/5] updated comments of *g theorems

---
 set.mm | 105 ++++++++++++++++++++++++++++++++++-----------------------
 1 file changed, 62 insertions(+), 43 deletions(-)

diff --git a/set.mm b/set.mm
index 5823477e62..e462086050 100644
--- a/set.mm
+++ b/set.mm
@@ -25103,8 +25103,9 @@ yield an eliminable and weakly (that is, object-level) conservative
   ${
     $d x z $.
     hbabg.1 $e |- ( ph -> A. x ph ) $.
-    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by NM, 1-Mar-1995.) $)
+    $( Bound-variable hypothesis builder for a class abstraction.  See ~ hbab
+       for a version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by NM, 1-Mar-1995.) $)
     hbabg $p |- ( z e. { y | ph } -> A. x z e. { y | ph } ) $=
       ( cv cab wcel wsb df-clab hbsb hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
   $}
@@ -25124,8 +25125,9 @@ yield an eliminable and weakly (that is, object-level) conservative
   ${
     $d x z $.
     nfsabg.1 $e |- F/ x ph $.
-    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by Mario Carneiro, 11-Aug-2016.) $)
+    $( Bound-variable hypothesis builder for a class abstraction.  See ~ nfsab
+       for a version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.) $)
     nfsabg $p |- F/ x z e. { y | ph } $=
       ( cv cab wcel nf5ri hbabg nf5i ) DFACGHBABCDABEIJK $.
   $}
@@ -26655,8 +26657,10 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d y A $.  $d x z $.
     hblemg.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Change the free variable of a hypothesis builder.  (Contributed by NM,
-       21-Jun-1993.)  (Revised by Andrew Salmon, 11-Jul-2011.) $)
+    $( Change the free variable of a hypothesis builder.  See ~ hblem for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
+       11-Jul-2011.) $)
     hblemg $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ
       BCDKZOPAQLM $.
@@ -27083,8 +27087,9 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d x z $.  $d y z $.  $d z ph $.
     nfabg.1 $e |- F/ x ph $.
-    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by Mario Carneiro, 11-Aug-2016.) $)
+    $( Bound-variable hypothesis builder for a class abstraction.  See ~ nfab
+       for a version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.) $)
     nfabg $p |- F/_ x { y | ph } $=
       ( vz cab nfsabg nfci ) BEACFABCEDGH $.
   $}
@@ -27100,8 +27105,9 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
     $( $j usage 'nfaba1' avoids 'ax-13'; $)
   $}
 
-  $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-     by Mario Carneiro, 14-Oct-2016.) $)
+  $( Bound-variable hypothesis builder for a class abstraction.  See ~ nfaba1
+     for a version with disjoint variable conditions, but not requiring
+     ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.) $)
   nfaba1g $p |- F/_ x { y | A. x ph } $=
     ( wal nfa1 nfabg ) ABDBCABEF $.
 
@@ -29821,8 +29827,9 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     nfrexdg.1 $e |- F/ y ph $.
     nfrexdg.2 $e |- ( ph -> F/_ x A ) $.
     nfrexdg.3 $e |- ( ph -> F/ x ps ) $.
-    $( Deduction version of ~ nfrexg .  (Contributed by Mario Carneiro,
-       14-Oct-2016.) $)
+    $( Deduction version of ~ nfrexg .  See ~ nfrexd for a version with
+       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
+       by Mario Carneiro, 14-Oct-2016.) $)
     nfrexdg $p |- ( ph -> F/ x E. y e. A ps ) $=
       ( wrex wn wral dfrex2 nfnd nfrald nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGAB
       CHMNMO $.
@@ -29847,9 +29854,11 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
   ${
     nfrexg.1 $e |- F/_ x A $.
     nfrexg.2 $e |- F/ x ph $.
-    $( Bound-variable hypothesis builder for restricted quantification.
-       (Contributed by NM, 1-Sep-1999.)  (Revised by Mario Carneiro,
-       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 30-Dec-2019.) $)
+    $( Bound-variable hypothesis builder for restricted quantification.  See
+       ~ nfrex for a version with disjoint variable conditions, but not
+       requiring ~ ax-13 .  (Contributed by NM, 1-Sep-1999.)  (Revised by Mario
+       Carneiro, 7-Oct-2016.)  (Proof shortened by Wolf Lammen,
+       30-Dec-2019.) $)
     nfrexg $p |- F/ x E. y e. A ph $=
       ( wrex wnf wtru nftru wnfc a1i nfrexdg mptru ) ACDGBHIABCDCJBDKIELABHIFLM
       N $.
@@ -44865,14 +44874,16 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $d z A $.  $d z B $.  $d x z $.  $d y z $.
     nfiung.1 $e |- F/_ y A $.
     nfiung.2 $e |- F/_ y B $.
-    $( Bound-variable hypothesis builder for indexed union.  (Contributed by
-       Mario Carneiro, 25-Jan-2014.) $)
+    $( Bound-variable hypothesis builder for indexed union.  See ~ nfiun for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.) $)
     nfiung $p |- F/_ y U_ x e. A B $=
       ( vz ciun cv wcel wrex cab df-iun nfcri nfrexg nfabg nfcxfr ) BACDHGIDJZA
       CKZGLAGCDMSBGRBACEBGDFNOPQ $.
 
-    $( Bound-variable hypothesis builder for indexed intersection.
-       (Contributed by Mario Carneiro, 25-Jan-2014.) $)
+    $( Bound-variable hypothesis builder for indexed intersection.  See ~ nfiin
+       for a version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.) $)
     nfiing $p |- F/_ y |^|_ x e. A B $=
       ( vz ciin cv wcel wral cab df-iin nfcri nfral nfabg nfcxfr ) BACDHGIDJZAC
       KZGLAGCDMSBGRBACEBGDFNOPQ $.
@@ -44999,15 +45010,19 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     cbviung.2 $e |- F/_ x C $.
     cbviung.3 $e |- ( x = y -> B = C ) $.
     $( Rule used to change the bound variables in an indexed union, with the
-       substitution specified implicitly by the hypothesis.  (Contributed by
-       NM, 26-Mar-2006.)  (Revised by Andrew Salmon, 25-Jul-2011.) $)
+       substitution specified implicitly by the hypothesis.  See ~ cbviun for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by NM, 26-Mar-2006.)  (Revised by Andrew Salmon,
+       25-Jul-2011.) $)
     cbviung $p |- U_ x e. A B = U_ y e. A C $=
       ( vz cv wcel wrex cab ciun nfcri weq eleq2d cbvrex abbii df-iun 3eqtr4i )
       IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBICE
       TUA $.
 
-    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
-       Hankins, 26-Aug-2009.)  (Revised by Mario Carneiro, 14-Oct-2016.) $)
+    $( Change bound variables in an indexed intersection.  See ~ cbviin for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.)  (Revised by
+       Mario Carneiro, 14-Oct-2016.) $)
     cbviing $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( vz cv wcel wral cab ciin nfcri weq eleq2d cbvral abbii df-iin 3eqtr4i )
       IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBICE
@@ -45018,18 +45033,16 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $d x y A $.  $d y B $.  $d x C $.
     cbviunv.1 $e |- ( x = y -> B = C ) $.
     $( Rule used to change the bound variables in an indexed union, with the
-       substitution specified implicitly by the hypothesis.  (Contributed by
-       NM, 15-Sep-2003.)  Add disjoint variable condition to avoid ~ ax-13 .
-       See ~ cbviunvg for a less restrictive version requiring more axioms.
-       (Revised by Gino Giotto, 20-Jan-2024.) $)
+       substitution specified implicitly by the hypothesis.  See ~ cbviunv for
+       a version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviunv' avoids 'ax-13'; $)
 
-    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
-       Hankins, 26-Aug-2009.)  Add disjoint variable condition to avoid
-       ~ ax-13 .  See ~ cbviinvg for a less restrictive version requiring more
-       axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
+    $( Change bound variables in an indexed intersection.  See ~ cbviinv for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.) $)
     cbviinv $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( nfcv cbviin ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviinv' avoids 'ax-13'; $)
@@ -46727,8 +46740,9 @@ although the definition does not require it (see ~ dfid2 for a case
     cbvopab1g.2 $e |- F/ x ps $.
     cbvopab1g.3 $e |- ( x = z -> ( ph <-> ps ) ) $.
     $( Change first bound variable in an ordered-pair class abstraction, using
-       explicit substitution.  (Contributed by NM, 6-Oct-2004.)  (Revised by
-       Mario Carneiro, 14-Oct-2016.) $)
+       explicit substitution.  See ~ cbvopab1 for a version with more disjoint
+       variable conditions, but not requiring ~ ax-13 .  (Contributed by NM,
+       6-Oct-2004.)  (Revised by Mario Carneiro, 14-Oct-2016.) $)
     cbvopab1g $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
       ( vw vv cv cop wceq wa wex cab copab wsb nfv nfan nfs1v nfex opeq1 eqeq2d
       sbequ12 anbi12d exbidv cbvexv1 nfsb sbequ sbie syl6bb bitri abbii df-opab
@@ -47017,8 +47031,9 @@ although the definition does not require it (see ~ dfid2 for a case
     cbvmptfg.5 $e |- ( x = y -> B = C ) $.
     $( Rule to change the bound variable in a maps-to function, using implicit
        substitution.  This version has bound-variable hypotheses in place of
-       distinct variable conditions.  (Contributed by NM, 11-Sep-2011.)
-       (Revised by Thierry Arnoux, 9-Mar-2017.) $)
+       distinct variable conditions.  See ~ cbvmptf for a version with more
+       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
+       by NM, 11-Sep-2011.)  (Revised by Thierry Arnoux, 9-Mar-2017.) $)
     cbvmptfg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( vz vw cv wcel wceq wa copab cmpt wsb weq nfv nfcri nfs1v eleq1w sbequ12
       nfan anbi12d cbvopab1g nfeq2 nfsb sbequ eqeq2d sbie syl6bb df-mpt 3eqtr4i
@@ -47051,7 +47066,9 @@ although the definition does not require it (see ~ dfid2 for a case
     cbvmptg.3 $e |- ( x = y -> B = C ) $.
     $( Rule to change the bound variable in a maps-to function, using implicit
        substitution.  This version has bound-variable hypotheses in place of
-       distinct variable conditions.  (Contributed by NM, 11-Sep-2011.) $)
+       distinct variable conditions.  See ~ cbvmpt for a version with more
+       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
+       by NM, 11-Sep-2011.) $)
     cbvmptg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( nfcv cbvmptfg ) ABCDEACIBCIFGHJ $.
   $}
@@ -47073,7 +47090,9 @@ although the definition does not require it (see ~ dfid2 for a case
     $d A x $.  $d A y $.  $d B y $.  $d C x $.
     cbvmptvg.1 $e |- ( x = y -> B = C ) $.
     $( Rule to change the bound variable in a maps-to function, using implicit
-       substitution.  (Contributed by Mario Carneiro, 19-Feb-2013.) $)
+       substitution.  See ~ cbvmptv for a version with more disjoint variable
+       conditions, but not requiring ~ ax-13 .  (Contributed by Mario Carneiro,
+       19-Feb-2013.) $)
     cbvmptvg $p |- ( x e. A |-> B ) = ( y e. A |-> C ) $=
       ( nfcv cbvmptg ) ABCDEBDGAEGFH $.
   $}
@@ -497243,10 +497262,9 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
     $d x y $.  $d y z $.
     bnj1441.1 $e |- ( x e. A -> A. y x e. A ) $.
     bnj1441.2 $e |- ( ph -> A. y ph ) $.
-    $( First-order logic and set theory.  (Contributed by Jonathan Ben-Naim,
-       3-Jun-2011.)  Add disjoint variable condition to avoid ~ ax-13 .  See
-       ~ bnj1441g for a less restrictive version requiring more axioms.
-       (Revised by Gino Giotto, 20-Jan-2024.)  (New usage is discouraged.) $)
+    $( First-order logic and set theory.  See ~ bnj1441 for a version with more
+       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
+       by Jonathan Ben-Naim, 3-Jun-2011.)  (New usage is discouraged.) $)
     bnj1441 $p |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) $=
       ( crab cv wcel wa cab df-rab hban hbab hbxfreq ) CDABEHBIEJZAKZBLABEMRCBD
       QACFGNOP $.
@@ -752388,8 +752406,9 @@ coordinates of the intersection points of a (nondegenerate) line and a
     nfiundg.1 $e |- F/ x ph $.
     nfiundg.2 $e |- ( ph -> F/_ y A ) $.
     nfiundg.3 $e |- ( ph -> F/_ y B ) $.
-    $( Bound-variable hypothesis builder for indexed union.  (Contributed by
-       Emmett Weisz, 6-Dec-2019.) $)
+    $( Bound-variable hypothesis builder for indexed union.  See ~ nfiund for a
+       version with more disjoint variable conditions, but not requiring
+       ~ ax-13 .  (Contributed by Emmett Weisz, 6-Dec-2019.) $)
     nfiundg $p |- ( ph -> F/_ y U_ x e. A B ) $=
       ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexdg nfabd nfcxfrd ) ACBDE
       JIKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.

From 993dc8a89eaa52f8844f1f12824d465b1b60bdf7 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 27 Jan 2024 13:05:31 +0100
Subject: [PATCH 4/5] mistake correction

---
 set.mm | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/set.mm b/set.mm
index e462086050..700687f44b 100644
--- a/set.mm
+++ b/set.mm
@@ -45033,16 +45033,18 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $d x y A $.  $d y B $.  $d x C $.
     cbviunv.1 $e |- ( x = y -> B = C ) $.
     $( Rule used to change the bound variables in an indexed union, with the
-       substitution specified implicitly by the hypothesis.  See ~ cbviunv for
-       a version with more disjoint variable conditions, but not requiring
-       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.) $)
+       substitution specified implicitly by the hypothesis.  (Contributed by
+       NM, 15-Sep-2003.)  Add disjoint variable condition to avoid ~ ax-13 .
+       See ~ cbviunvg for a less restrictive version requiring more axioms.
+       (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviunv' avoids 'ax-13'; $)
 
-    $( Change bound variables in an indexed intersection.  See ~ cbviinv for a
-       version with more disjoint variable conditions, but not requiring
-       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.) $)
+    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
+       Hankins, 26-Aug-2009.)  Add disjoint variable condition to avoid
+       ~ ax-13 .  See ~ cbviinvg for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviinv $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( nfcv cbviin ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviinv' avoids 'ax-13'; $)

From 7cdb3d9fa49ac8ce504aae1647daa0ebb8bc3057 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 27 Jan 2024 13:18:00 +0100
Subject: [PATCH 5/5] correction

---
 set.mm | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/set.mm b/set.mm
index 700687f44b..50122e5a1b 100644
--- a/set.mm
+++ b/set.mm
@@ -497264,9 +497264,10 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
     $d x y $.  $d y z $.
     bnj1441.1 $e |- ( x e. A -> A. y x e. A ) $.
     bnj1441.2 $e |- ( ph -> A. y ph ) $.
-    $( First-order logic and set theory.  See ~ bnj1441 for a version with more
-       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
-       by Jonathan Ben-Naim, 3-Jun-2011.)  (New usage is discouraged.) $)
+    $( First-order logic and set theory.  (Contributed by Jonathan Ben-Naim,
+       3-Jun-2011.)  Add disjoint variable condition to avoid ~ ax-13 .  See
+       ~ bnj1441g for a less restrictive version requiring more axioms.
+       (Revised by Gino Giotto, 20-Jan-2024.)  (New usage is discouraged.) $)
     bnj1441 $p |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) $=
       ( crab cv wcel wa cab df-rab hban hbab hbxfreq ) CDABEHBIEJZAKZBLABEMRCBD
       QACFGNOP $.
@@ -497276,8 +497277,9 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
     $d y z $.
     bnj1441g.1 $e |- ( x e. A -> A. y x e. A ) $.
     bnj1441g.2 $e |- ( ph -> A. y ph ) $.
-    $( First-order logic and set theory.  (Contributed by Jonathan Ben-Naim,
-       3-Jun-2011.)  (New usage is discouraged.) $)
+    $( First-order logic and set theory.  See ~ bnj1441 for a version with more
+       disjoint variable conditions, but not requiring ~ ax-13 .  (Contributed
+       by Jonathan Ben-Naim, 3-Jun-2011.)  (New usage is discouraged.) $)
     bnj1441g $p |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) $=
       ( crab cv wcel wa cab df-rab hban hbabg hbxfreq ) CDABEHBIEJZAKZBLABEMRCB
       DQACFGNOP $.