From 4f221c9511be093c77451a35535b5eaae75a80e6 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 20 Jan 2024 18:05:42 +0100
Subject: [PATCH 1/6] reduced ax-13 usage

---
 discouraged |  41 ++++++
 set.mm      | 362 ++++++++++++++++++++++++++++++++++------------------
 2 files changed, 277 insertions(+), 126 deletions(-)

diff --git a/discouraged b/discouraged
index 36beba9f30..2a3fae16a8 100755
--- a/discouraged
+++ b/discouraged
@@ -2998,6 +2998,8 @@
 "cbncms" is used by "ubthlem2".
 "cbvexsv" is used by "onfrALTlem1".
 "cbvexsv" is used by "onfrALTlem1VD".
+"cbviinALT" is used by "cbviinvALT".
+"cbviunALT" is used by "cbviunvALT".
 "cbvmptALT" is used by "cbvmptvALT".
 "cbvmptfALT" is used by "cbvmptALT".
 "cbvopab1ALT" is used by "cbvmptfALT".
@@ -6342,6 +6344,8 @@
 "hba1-o" is used by "axc711toc7".
 "hba1-o" is used by "dvelimf-o".
 "hba1-o" is used by "nfa1-o".
+"hbabALT" is used by "bnj1441ALT".
+"hbabALT" is used by "nfsabALT".
 "hbae-o" is used by "aev-o".
 "hbae-o" is used by "dral1-o".
 "hbae-o" is used by "dral2-o".
@@ -9525,6 +9529,13 @@
 "nfa1-o" is used by "ax12eq".
 "nfa1-o" is used by "ax12v2-o".
 "nfa1-o" is used by "axc11n-16".
+"nfabALT" is used by "nfaba1ALT".
+"nfabALT" is used by "nfiinALT".
+"nfabALT" is used by "nfiunALT".
+"nfrexALT" is used by "nfiunALT".
+"nfrexdALT" is used by "nfiundALT".
+"nfrexdALT" is used by "nfrexALT".
+"nfsabALT" is used by "nfabALT".
 "nfsb2ALT" is used by "nfsb4tALT".
 "nfsb4ALT" is used by "sbco2ALT".
 "nfsb4tALT" is used by "nfsb4ALT".
@@ -13814,6 +13825,7 @@ New usage of "bnj1423" is discouraged (1 uses).
 New usage of "bnj1424" is discouraged (2 uses).
 New usage of "bnj1436" is discouraged (12 uses).
 New usage of "bnj1441" is discouraged (0 uses).
+New usage of "bnj1441ALT" is discouraged (0 uses).
 New usage of "bnj1442" is discouraged (1 uses).
 New usage of "bnj1444" is discouraged (1 uses).
 New usage of "bnj1445" is discouraged (1 uses).
@@ -14063,6 +14075,10 @@ 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 "cbviinALT" is discouraged (1 uses).
+New usage of "cbviinvALT" is discouraged (0 uses).
+New usage of "cbviunALT" is discouraged (1 uses).
+New usage of "cbviunvALT" 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).
@@ -15385,6 +15401,7 @@ New usage of "hatomic" is discouraged (1 uses).
 New usage of "hatomici" is discouraged (6 uses).
 New usage of "hatomistici" is discouraged (1 uses).
 New usage of "hba1-o" is discouraged (8 uses).
+New usage of "hbabALT" is discouraged (2 uses).
 New usage of "hbae-o" is discouraged (4 uses).
 New usage of "hbalg" is discouraged (1 uses).
 New usage of "hbalgVD" is discouraged (0 uses).
@@ -15393,6 +15410,7 @@ New usage of "hbexg" is discouraged (0 uses).
 New usage of "hbexgVD" is discouraged (0 uses).
 New usage of "hbimpg" is discouraged (0 uses).
 New usage of "hbimpgVD" is discouraged (0 uses).
+New usage of "hblemALT" is discouraged (0 uses).
 New usage of "hbnae-o" is discouraged (3 uses).
 New usage of "hbntal" is discouraged (3 uses).
 New usage of "hbra2VD" is discouraged (0 uses).
@@ -16385,14 +16403,22 @@ New usage of "nelne2OLD" is discouraged (0 uses).
 New usage of "nf5rOLD" is discouraged (0 uses).
 New usage of "nf5riOLD" is discouraged (0 uses).
 New usage of "nfa1-o" is discouraged (4 uses).
+New usage of "nfabALT" is discouraged (3 uses).
+New usage of "nfaba1ALT" is discouraged (0 uses).
 New usage of "nfabd2OLD" is discouraged (0 uses).
 New usage of "nfabdOLD" is discouraged (0 uses).
 New usage of "nfceqiOLD" is discouraged (0 uses).
 New usage of "nfcvfOLD" is discouraged (0 uses).
 New usage of "nfequid-o" is discouraged (0 uses).
 New usage of "nfeu1ALT" is discouraged (0 uses).
+New usage of "nfiinALT" is discouraged (0 uses).
+New usage of "nfiunALT" is discouraged (0 uses).
+New usage of "nfiundALT" is discouraged (0 uses).
 New usage of "nfopdALT" is discouraged (0 uses).
+New usage of "nfrexALT" is discouraged (1 uses).
+New usage of "nfrexdALT" is discouraged (2 uses).
 New usage of "nfsab1OLD" is discouraged (0 uses).
+New usage of "nfsabALT" is discouraged (1 uses).
 New usage of "nfsb2ALT" is discouraged (1 uses).
 New usage of "nfsb4ALT" is discouraged (1 uses).
 New usage of "nfsb4tALT" is discouraged (1 uses).
@@ -18204,6 +18230,7 @@ Proof modification of "bj-xpima1snALT" is discouraged (25 steps).
 Proof modification of "bj-xpima2sn" is discouraged (23 steps).
 Proof modification of "bj-xpnzex" is discouraged (71 steps).
 Proof modification of "bj-zfauscl" is discouraged (65 steps).
+Proof modification of "bnj1441ALT" is discouraged (30 steps).
 Proof modification of "brfi1indALT" is discouraged (789 steps).
 Proof modification of "brfvidRP" is discouraged (92 steps).
 Proof modification of "c0exALT" is discouraged (15 steps).
@@ -18217,6 +18244,10 @@ 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 "cbviinALT" is discouraged (64 steps).
+Proof modification of "cbviinvALT" is discouraged (13 steps).
+Proof modification of "cbviunALT" is discouraged (64 steps).
+Proof modification of "cbviunvALT" is discouraged (13 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).
@@ -18785,6 +18816,7 @@ Proof modification of "gsumccatOLD" is discouraged (995 steps).
 Proof modification of "hadcomaOLD" is discouraged (37 steps).
 Proof modification of "hashge3el3dif" is discouraged (229 steps).
 Proof modification of "hba1-o" is discouraged (34 steps).
+Proof modification of "hbabALT" is discouraged (22 steps).
 Proof modification of "hbae-o" is discouraged (85 steps).
 Proof modification of "hbalg" is discouraged (31 steps).
 Proof modification of "hbalgVD" is discouraged (53 steps).
@@ -18793,6 +18825,7 @@ Proof modification of "hbexg" is discouraged (71 steps).
 Proof modification of "hbexgVD" is discouraged (205 steps).
 Proof modification of "hbimpg" is discouraged (88 steps).
 Proof modification of "hbimpgVD" is discouraged (165 steps).
+Proof modification of "hblemALT" is discouraged (33 steps).
 Proof modification of "hbnae-o" is discouraged (11 steps).
 Proof modification of "hbntal" is discouraged (48 steps).
 Proof modification of "hbra2VD" is discouraged (26 steps).
@@ -18963,14 +18996,22 @@ Proof modification of "nelne2OLD" is discouraged (26 steps).
 Proof modification of "nf5rOLD" is discouraged (22 steps).
 Proof modification of "nf5riOLD" is discouraged (13 steps).
 Proof modification of "nfa1-o" is discouraged (8 steps).
+Proof modification of "nfabALT" is discouraged (12 steps).
+Proof modification of "nfaba1ALT" is discouraged (9 steps).
 Proof modification of "nfabd2OLD" is discouraged (75 steps).
 Proof modification of "nfabdOLD" is discouraged (18 steps).
 Proof modification of "nfceqiOLD" is discouraged (21 steps).
 Proof modification of "nfcvfOLD" is discouraged (18 steps).
 Proof modification of "nfequid-o" is discouraged (8 steps).
 Proof modification of "nfeu1ALT" is discouraged (25 steps).
+Proof modification of "nfiinALT" is discouraged (35 steps).
+Proof modification of "nfiunALT" is discouraged (35 steps).
+Proof modification of "nfiundALT" is discouraged (43 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
+Proof modification of "nfrexALT" is discouraged (27 steps).
+Proof modification of "nfrexdALT" is discouraged (34 steps).
 Proof modification of "nfsab1OLD" is discouraged (12 steps).
+Proof modification of "nfsabALT" is discouraged (17 steps).
 Proof modification of "nfsb2ALT" is discouraged (18 steps).
 Proof modification of "nfsb4ALT" is discouraged (23 steps).
 Proof modification of "nfsb4tALT" is discouraged (119 steps).
diff --git a/set.mm b/set.mm
index 78f6b857f6..3e33b5969a 100644
--- a/set.mm
+++ b/set.mm
@@ -19939,6 +19939,15 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
       N $.
   $}
 
+  ${
+    $d x z $.  $d y z $.
+    hbsbw.1 $e |- ( ph -> A. z ph ) $.
+    $( Version of ~ hbsb with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
+    hbsbw $p |- ( [ y / x ] ph -> A. z [ y / x ] ph ) $=
+      ( wsb nf5i nfsbv nf5ri ) ABCFDABCDADEGHI $.
+  $}
+
   ${
     $d x z $.  $d y z $.
     sbco2v.1 $e |- F/ z ph $.
@@ -25076,23 +25085,45 @@ yield an eliminable and weakly (that is, object-level) conservative
   $}
 
   ${
-    $d x z $.
+    $d x y $.  $d x z $.
     hbab.1 $e |- ( ph -> A. x ph ) $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by NM, 1-Mar-1995.) $)
+       by NM, 1-Mar-1995.)  Add disjoint variable condition to avoid ~ ax-13 .
+       (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 hbsb hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
+      ( cv cab wcel wsb df-clab hbsbw hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
   $}
 
   ${
     $d x z $.
+    hbabALT.1 $e |- ( ph -> A. x ph ) $.
+    $( Alternate version of ~ hbab , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by NM, 1-Mar-1995.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    hbabALT $p |- ( z e. { y | ph } -> A. x z e. { y | ph } ) $=
+      ( cv cab wcel wsb df-clab hbsb hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
+  $}
+
+  ${
+    $d x y $.  $d x z $.
     nfsab.1 $e |- F/ x ph $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by Mario Carneiro, 11-Aug-2016.) $)
+       by Mario Carneiro, 11-Aug-2016.)  Add disjoint variable condition to
+       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfsab $p |- F/ x z e. { y | ph } $=
       ( cv cab wcel nf5ri hbab nf5i ) DFACGHBABCDABEIJK $.
   $}
 
+  ${
+    $d x z $.
+    nfsabALT.1 $e |- F/ x ph $.
+    $( Alternate version of ~ nfsab , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfsabALT $p |- F/ x z e. { y | ph } $=
+      ( cv cab wcel nf5ri hbabALT nf5i ) DFACGHBABCDABEIJK $.
+  $}
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -26603,12 +26634,24 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   $}
 
   ${
-    $d y A $.  $d x z $.
+    $d y A $.  $d x z $.  $d x y $.
     hblem.1 $e |- ( y e. A -> A. x y e. A ) $.
     $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
        (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.) $)
+       11-Jul-2011.)  Add disjoint variable condition to avoid ~ ax-13 .
+       (Revised by Gino Giotto, 20-Jan-2024.) $)
     hblem $p |- ( z e. A -> A. x z e. A ) $=
+      ( cv wcel wsb wal hbsbw clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAE
+      JBCDKZOPAQLM $.
+  $}
+
+  ${
+    $d y A $.  $d x z $.
+    hblemALT.1 $e |- ( y e. A -> A. x y e. A ) $.
+    $( Alternate version of ~ hblem , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    hblemALT $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ
       BCDKZOPAQLM $.
   $}
@@ -27020,18 +27063,39 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   $}
 
   ${
-    $d x z $.  $d y z $.  $d z ph $.
+    $d x y z $.  $d z ph $.
     nfab.1 $e |- F/ x ph $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-       by Mario Carneiro, 11-Aug-2016.) $)
+       by Mario Carneiro, 11-Aug-2016.)  Add disjoint variable condition to
+       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfab $p |- F/_ x { y | ph } $=
       ( vz cab nfsab nfci ) BEACFABCEDGH $.
   $}
 
-  $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
-     by Mario Carneiro, 14-Oct-2016.) $)
-  nfaba1 $p |- F/_ x { y | A. x ph } $=
-    ( wal nfa1 nfab ) ABDBCABEF $.
+  ${
+    $d x z $.  $d y z $.  $d z ph $.
+    nfabALT.1 $e |- F/ x ph $.
+    $( Alternate version of ~ nfab , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfabALT $p |- F/_ x { y | ph } $=
+      ( vz cab nfsabALT nfci ) BEACFABCEDGH $.
+  $}
+
+  ${
+    $d x y $.
+    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
+       by Mario Carneiro, 14-Oct-2016.)  Add disjoint variable condition to
+       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+    nfaba1 $p |- F/_ x { y | A. x ph } $=
+      ( wal nfa1 nfab ) ABDBCABEF $.
+  $}
+
+  $( Alternate version of ~ nfaba1 , with less dv conditions, but requiring
+     ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.)
+     (Proof modification is discouraged.)  (New usage is discouraged.) $)
+  nfaba1ALT $p |- F/_ x { y | A. x ph } $=
+    ( wal nfa1 nfabALT ) ABDBCABEF $.
 
   ${
     $d x y $.  $d y A $.  $d y B $.  $d y ph $.
@@ -27129,6 +27193,21 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
       GJZDKZCLZGITEKZCLZGICDMCEMSUBUDGUAUCABCSDETFNOPCGDQCGEQR $.
   $}
 
+  ${
+    $d x y z $.  $d z ph $.  $d z ps $.
+    nfabdw.1 $e |- F/ y ph $.
+    nfabdw.2 $e |- ( ph -> F/ x ps ) $.
+    $( Version of ~ nfabd with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
+    nfabdw $p |- ( ph -> F/_ x { y | ps } ) $=
+      ( vz cab nfv cv wcel wsb df-clab wnf wal alrimi wi weq nfim1 nfal nfa1 wb
+      sb6 biimpri axc4i syl6bi nf5d sbequ12 imbi2d equsalv bicomi nfnf1 sp nfim
+      a1i nfxfr pm5.5 nfbidf mpbii syl nfxfrd nfcd ) ACGBDHZAGIGJVCKBDGLZACBGDM
+      ABCNZDOZVDCNZAVEDEFPVFVFVDQZCNVGVHDGRZVFBQZQZDOZCVLVHVJVHDGVFVDDVEDUAZVFV
+      DDVMVFVDVIBQZDOZVDDOVDVOUBVFBDGUCZUOVNVDDVDVOVPUDUEUFUGSVIBVDVFBDGUHUIUJU
+      KVKCDVIVJCVICIVFBCVECDBCULTZVEDUMSUNTUPVFVHVDCVQVFVDUQURUSUTVAVB $.
+  $}
+
   ${
     $d x z $.  $d y z $.  $d z ph $.  $d z ps $.
     nfabd.1 $e |- F/ y ph $.
@@ -29710,27 +29789,56 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     ( wrex cv wcel wa wex df-rex nfe1 nfxfr ) ABCDBECFAGZBHBABCILBJK $.
 
   ${
+    $d x y $.
     nfrexd.1 $e |- F/ y ph $.
     nfrexd.2 $e |- ( ph -> F/_ x A ) $.
     nfrexd.3 $e |- ( ph -> F/ x ps ) $.
     $( Deduction version of ~ nfrex .  (Contributed by Mario Carneiro,
-       14-Oct-2016.) $)
+       14-Oct-2016.)  Add disjoint variable condition to avoid ~ ax-13 .
+       (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfrexd $p |- ( ph -> F/ x E. y e. A ps ) $=
+      ( wrex wn wral dfrex2 nfnd nfraldw nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGA
+      BCHMNMO $.
+  $}
+
+  ${
+    nfrexdALT.1 $e |- F/ y ph $.
+    nfrexdALT.2 $e |- ( ph -> F/_ x A ) $.
+    nfrexdALT.3 $e |- ( ph -> F/ x ps ) $.
+    $( Alternate version of ~ nfrexd , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfrexdALT $p |- ( ph -> F/ x E. y e. A ps ) $=
       ( wrex wn wral dfrex2 nfnd nfrald nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGAB
       CHMNMO $.
   $}
 
   ${
+    $d x y $.
     nfrex.1 $e |- F/_ x A $.
     nfrex.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.) $)
+       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 30-Dec-2019.)  Add
+       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
     nfrex $p |- F/ x E. y e. A ph $=
       ( wrex wnf wtru nftru wnfc a1i nfrexd mptru ) ACDGBHIABCDCJBDKIELABHIFLMN
       $.
   $}
 
+  ${
+    nfrexALT.1 $e |- F/_ x A $.
+    nfrexALT.2 $e |- F/ x ph $.
+    $( Alternate version of ~ nfrex , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by NM, 1-Sep-1999.)  (Revised by Mario Carneiro,
+       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 30-Dec-2019.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfrexALT $p |- F/ x E. y e. A ph $=
+      ( wrex wnf wtru nftru wnfc a1i nfrexdALT mptru ) ACDGBHIABCDCJBDKIELABHIF
+      LMN $.
+  $}
+
   ${
     reximdai.1 $e |- F/ x ph $.
     reximdai.2 $e |- ( ph -> ( x e. A -> ( ps -> ch ) ) ) $.
@@ -44716,20 +44824,41 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
   $}
 
   ${
-    $d z A $.  $d z B $.  $d x z $.  $d y z $.
+    $d x y z $.  $d z A $.  $d z B $.
     nfiun.1 $e |- F/_ y A $.
     nfiun.2 $e |- F/_ y B $.
     $( Bound-variable hypothesis builder for indexed union.  (Contributed by
-       Mario Carneiro, 25-Jan-2014.) $)
+       Mario Carneiro, 25-Jan-2014.)  Add disjoint variable condition to avoid
+       ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfiun $p |- F/_ y U_ x e. A B $=
       ( vz ciun cv wcel wrex cab df-iun nfcri nfrex nfab nfcxfr ) BACDHGIDJZACK
       ZGLAGCDMSBGRBACEBGDFNOPQ $.
 
     $( Bound-variable hypothesis builder for indexed intersection.
-       (Contributed by Mario Carneiro, 25-Jan-2014.) $)
+       (Contributed by Mario Carneiro, 25-Jan-2014.)  Add disjoint variable
+       condition to avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfiin $p |- F/_ y |^|_ x e. A B $=
-      ( vz ciin cv wcel wral cab df-iin nfcri nfral nfab nfcxfr ) BACDHGIDJZACK
-      ZGLAGCDMSBGRBACEBGDFNOPQ $.
+      ( vz ciin cv wcel wral cab df-iin nfcri nfralw nfab nfcxfr ) BACDHGIDJZAC
+      KZGLAGCDMSBGRBACEBGDFNOPQ $.
+  $}
+
+  ${
+    $d z A $.  $d z B $.  $d x z $.  $d y z $.
+    nfiunALT.1 $e |- F/_ y A $.
+    nfiunALT.2 $e |- F/_ y B $.
+    $( Alternate version of ~ nfiun , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfiunALT $p |- F/_ y U_ x e. A B $=
+      ( vz ciun cv wcel wrex cab df-iun nfcri nfrexALT nfabALT nfcxfr ) BACDHGI
+      DJZACKZGLAGCDMSBGRBACEBGDFNOPQ $.
+
+    $( Alternate version of ~ nfiin , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfiinALT $p |- F/_ y |^|_ x e. A B $=
+      ( vz ciin cv wcel wral cab df-iin nfcri nfral nfabALT nfcxfr ) BACDHGIDJZ
+      ACKZGLAGCDMSBGRBACEBGDFNOPQ $.
   $}
 
   ${
@@ -44819,32 +44948,61 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
   $}
 
   ${
-    $d z y A $.  $d z x A $.  $d z B $.  $d z C $.
+    $d x y z A $.  $d z B $.  $d z C $.
     cbviun.1 $e |- F/_ y B $.
     cbviun.2 $e |- F/_ x C $.
     cbviun.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.) $)
+       NM, 26-Mar-2006.)  (Revised by Andrew Salmon, 25-Jul-2011.)  Add
+       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
     cbviun $p |- U_ x e. A B = U_ y e. A C $=
+      ( vz cv wcel wrex cab ciun nfcri weq eleq2d cbvrexw abbii df-iun 3eqtr4i
+      ) IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBI
+      CETUA $.
+
+    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
+       Hankins, 26-Aug-2009.)  (Revised by Mario Carneiro, 14-Oct-2016.)  Add
+       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
+    cbviin $p |- |^|_ x e. A B = |^|_ y e. A C $=
+      ( vz cv wcel wral cab ciin nfcri weq eleq2d cbvralw abbii df-iin 3eqtr4i
+      ) IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBI
+      CETUA $.
+  $}
+
+  ${
+    $d z y A $.  $d z x A $.  $d z B $.  $d z C $.
+    cbviunALT.1 $e |- F/_ y B $.
+    cbviunALT.2 $e |- F/_ x C $.
+    cbviunALT.3 $e |- ( x = y -> B = C ) $.
+    $( Alternate version of ~ cbviun , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by NM, 26-Mar-2006.)  (Revised by Andrew Salmon,
+       25-Jul-2011.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    cbviunALT $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.) $)
-    cbviin $p |- |^|_ x e. A B = |^|_ y e. A C $=
+    $( Alternate version of ~ cbviin , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.)  (Revised by
+       Mario Carneiro, 14-Oct-2016.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    cbviinALT $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( vz cv wcel wral cab ciin nfcri weq eleq2d cbvral abbii df-iin 3eqtr4i )
       IJZDKZACLZIMUBEKZBCLZIMACDNBCENUDUFIUCUEABCBIDFOAIEGOABPDEUBHQRSAICDTBICE
       TUA $.
   $}
 
   ${
-    $d x A $.  $d y A $.  $d y B $.  $d x C $.
+    $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.) $)
+       NM, 15-Sep-2003.)  Add disjoint variable condition to avoid ~ ax-13 .
+       (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
 
@@ -44854,6 +45012,23 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
       ( nfcv cbviin ) ABCDEBDGAEGFH $.
   $}
 
+  ${
+    $d x A $.  $d y A $.  $d y B $.  $d x C $.
+    cbviunvALT.1 $e |- ( x = y -> B = C ) $.
+    $( Alternate version of ~ cbviunv , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.)  Add disjoint variable
+       condition to avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbviunvALT $p |- U_ x e. A B = U_ y e. A C $=
+      ( nfcv cbviunALT ) ABCDEBDGAEGFH $.
+
+    $( Alternate version of ~ cbviinv , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    cbviinvALT $p |- |^|_ x e. A B = |^|_ y e. A C $=
+      ( nfcv cbviinALT ) ABCDEBDGAEGFH $.
+  $}
+
   ${
     $d x y C $.  $d y A $.  $d y B $.
     $( Subset theorem for an indexed union.  (Contributed by NM, 13-Sep-2003.)
@@ -496923,16 +497098,29 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
   $}
 
   ${
-    $d y z $.
+    $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.)  (New usage is discouraged.) $)
+       3-Jun-2011.)  Add disjoint variable condition to avoid ~ ax-13 .
+       (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 $.
   $}
 
+  ${
+    $d y z $.
+    bnj1441ALT.1 $e |- ( x e. A -> A. y x e. A ) $.
+    bnj1441ALT.2 $e |- ( ph -> A. y ph ) $.
+    $( Alternate version of ~ bnj1441 , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    bnj1441ALT $p |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) $=
+      ( crab cv wcel wa cab df-rab hban hbabALT hbxfreq ) CDABEHBIEJZAKZBLABEMR
+      CBDQACFGNOP $.
+  $}
+
   ${
     bnj1454.1 $e |- A = { x | ph } $.
     $( First-order logic and set theory.  (Contributed by Jonathan Ben-Naim,
@@ -501568,7 +501756,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
   $}
 
   ${
-    $d A y $.  $d G y $.  $d R y $.  $d x y $.  $d y z $.
+    $d A y $.  $d G y $.  $d R y $.  $d x y $.  $d y z $.  $d f y $.
     bnj1447.1 $e |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d )
         } $.
     bnj1447.2 $e |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. $.
@@ -502226,7 +502414,7 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
   $}
 
   ${
-    $d A d $.  $d G d $.  $d R d $.  $d d x $.
+    $d A d $.  $d G d $.  $d R d $.  $d d x $.  $d d f $.
     bnj1519.1 $e |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d )
         } $.
     bnj1519.2 $e |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. $.
@@ -630338,15 +630526,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       ( wsb weq sbiedvw sbievw ) ADEHBCFCFIABDEGJK $.
   $}
 
-  ${
-    $d x z $.  $d y z $.
-    hbsbw.1 $e |- ( ph -> A. z ph ) $.
-    $( Version of ~ hbsb with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    hbsbw $p |- ( [ y / x ] ph -> A. z [ y / x ] ph ) $=
-      ( wsb nf5i nfsbv nf5ri ) ABCFDABCDADEGHI $.
-  $}
-
   ${
     $d x ph $.  $d x ch $.  $d x y $.
     cbvaldw.1 $e |- F/ y ph $.
@@ -630469,34 +630648,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       ( weu wsb sb8euv sbiev eubii bitri ) ACHACDIZDHBDHACDEJNBDABCDFGKLM $.
   $}
 
-  ${
-    $d x z $.  $d x y $.
-    hbabw.1 $e |- ( ph -> A. x ph ) $.
-    $( Version of ~ hbab with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    hbabw $p |- ( z e. { y | ph } -> A. x z e. { y | ph } ) $=
-      ( cv cab wcel wsb df-clab hbsbw hbxfrbi ) DFACGHACDIBADCJACDBEKL $.
-  $}
-
-  ${
-    $d x z $.  $d x y $.
-    nfsabw.1 $e |- F/ x ph $.
-    $( Version of ~ nfsab with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfsabw $p |- F/ x z e. { y | ph } $=
-      ( cv cab wcel nf5ri hbabw nf5i ) DFACGHBABCDABEIJK $.
-  $}
-
-  ${
-    $d y A $.  $d x z $.  $d x y $.
-    hblemw.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Version of ~ hblem with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    hblemw $p |- ( z e. A -> A. x z e. A ) $=
-      ( cv wcel wsb wal hbsbw clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAE
-      JBCDKZOPAQLM $.
-  $}
-
   ${
     $d x y z $.  $d ph z $.  $d ps z $.
     cbvabw.1 $e |- F/ y ph $.
@@ -630519,38 +630670,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       GZABHBFCGNEBAAECDIJOPABEACKLEBCKM $.
   $}
 
-  ${
-    $d x y z $.  $d z ph $.
-    nfabw.1 $e |- F/ x ph $.
-    $( Version of ~ nfab with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfabw $p |- F/_ x { y | ph } $=
-      ( vz cab nfsabw nfci ) BEACFABCEDGH $.
-  $}
-
-  ${
-    $d x y $.
-    $( Version of ~ nfaba1 with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfaba1w $p |- F/_ x { y | A. x ph } $=
-      ( wal nfa1 nfabw ) ABDBCABEF $.
-  $}
-
-  ${
-    $d x y z $.  $d z ph $.  $d z ps $.
-    nfabdw.1 $e |- F/ y ph $.
-    nfabdw.2 $e |- ( ph -> F/ x ps ) $.
-    $( Version of ~ nfabd with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfabdw $p |- ( ph -> F/_ x { y | ps } ) $=
-      ( vz cab nfv cv wcel wsb df-clab wnf wal alrimi wi weq nfim1 nfal nfa1 wb
-      sb6 biimpri axc4i syl6bi nf5d sbequ12 imbi2d equsalv bicomi nfnf1 sp nfim
-      a1i nfxfr pm5.5 nfbidf mpbii syl nfxfrd nfcd ) ACGBDHZAGIGJVCKBDGLZACBGDM
-      ABCNZDOZVDCNZAVEDEFPVFVFVDQZCNVGVHDGRZVFBQZQZDOZCVLVHVJVHDGVFVDDVEDUAZVFV
-      DDVMVFVDVIBQZDOZVDDOVDVOUBVFBDGUCZUOVNVDDVDVOVPUDUEUFUGSVIBVDVFBDGUHUIUJU
-      KVKCDVIVJCVICIVFBCVECDBCULTZVEDUMSUNTUPVFVHVDCVQVFVDUQURUSUTVAVB $.
-  $}
-
   ${
     $d A y $.  $d x y $.
     $( Version of ~ nfra2 with a disjoint variable condition, which does not
@@ -630559,29 +630678,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       ( wral nfcv nfra1 nfralw ) ACEFCBDCDGACEHI $.
   $}
 
-  ${
-    $d x y $.
-    nfrexdw.1 $e |- F/ y ph $.
-    nfrexdw.2 $e |- ( ph -> F/_ x A ) $.
-    nfrexdw.3 $e |- ( ph -> F/ x ps ) $.
-    $( Version of ~ nfrexd with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfrexdw $p |- ( ph -> F/ x E. y e. A ps ) $=
-      ( wrex wn wral dfrex2 nfnd nfraldw nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGA
-      BCHMNMO $.
-  $}
-
-  ${
-    $d x y $.
-    nfrexw.1 $e |- F/_ x A $.
-    nfrexw.2 $e |- F/ x ph $.
-    $( Version of ~ nfrex with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    nfrexw $p |- F/ x E. y e. A ph $=
-      ( wrex wnf wtru nftru wnfc a1i nfrexdw mptru ) ACDGBHIABCDCJBDKIELABHIFLM
-      N $.
-  $}
-
   ${
     $d x y A $.
     $( Version of ~ ralcom2 with a disjoint variable condition, which does not
@@ -752042,15 +752138,29 @@ coordinates of the intersection points of a (nondegenerate) line and a
   $}
 
   ${
-    $d z ph $.  $d z A $.  $d z B $.  $d z x $.  $d z y $.
+    $d x y z $.  $d z ph $.  $d z A $.  $d z B $.
     nfiund.1 $e |- F/ x ph $.
     nfiund.2 $e |- ( ph -> F/_ y A ) $.
     nfiund.3 $e |- ( ph -> F/_ y B ) $.
     $( Bound-variable hypothesis builder for indexed union.  (Contributed by
-       Emmett Weisz, 6-Dec-2019.) $)
+       Emmett Weisz, 6-Dec-2019.)  Add disjoint variable condition to avoid
+       ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfiund $p |- ( ph -> F/_ y U_ x e. A B ) $=
-      ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexd nfabd nfcxfrd ) ACBDEJ
-      IKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.
+      ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexd nfabdw nfcxfrd ) ACBDE
+      JIKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.
+  $}
+
+  ${
+    $d z ph $.  $d z A $.  $d z B $.  $d z x $.  $d z y $.
+    nfiundALT.1 $e |- F/ x ph $.
+    nfiundALT.2 $e |- ( ph -> F/_ y A ) $.
+    nfiundALT.3 $e |- ( ph -> F/_ y B ) $.
+    $( Alternate version of ~ nfiund , with less dv conditions, but requiring
+       ~ ax-13 .  (Contributed by Emmett Weisz, 6-Dec-2019.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    nfiundALT $p |- ( ph -> F/_ y U_ x e. A B ) $=
+      ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexdALT nfabd nfcxfrd ) ACB
+      DEJIKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.
   $}
 
   $( ${

From aae13a869a5b57509876c28ddfbb7f4bbcacb354 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 20 Jan 2024 18:59:12 +0100
Subject: [PATCH 2/6] more accurate comment

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

diff --git a/set.mm b/set.mm
index 3e33b5969a..0145e2a630 100644
--- a/set.mm
+++ b/set.mm
@@ -27091,7 +27091,7 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
       ( wal nfa1 nfab ) ABDBCABEF $.
   $}
 
-  $( Alternate version of ~ nfaba1 , with less dv conditions, but requiring
+  $( Alternate version of ~ nfaba1 , with no dv conditions, but requiring
      ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.)
      (Proof modification is discouraged.)  (New usage is discouraged.) $)
   nfaba1ALT $p |- F/_ x { y | A. x ph } $=

From 18a3176b4bd30b7adfd32f5605bf1a529aafc149 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sat, 20 Jan 2024 19:25:41 +0100
Subject: [PATCH 3/6] comment correction

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

diff --git a/set.mm b/set.mm
index 0145e2a630..db797e0183 100644
--- a/set.mm
+++ b/set.mm
@@ -45016,9 +45016,9 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $d x A $.  $d y A $.  $d y B $.  $d x C $.
     cbviunvALT.1 $e |- ( x = y -> B = C ) $.
     $( Alternate version of ~ cbviunv , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.)  Add disjoint variable
-       condition to avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.)  (Revised by Gino Giotto,
+       20-Jan-2024.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
     cbviunvALT $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviunALT ) ABCDEBDGAEGFH $.
 

From 6c2d564f483bd422bfdbc52e0b70c6d808a3ec67 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Tue, 23 Jan 2024 00:22:38 +0100
Subject: [PATCH 4/6] converted *ALT suffix into *g

---
 discouraged |  42 +---------
 set.mm      | 228 ++++++++++++++++++++++++++--------------------------
 2 files changed, 116 insertions(+), 154 deletions(-)

diff --git a/discouraged b/discouraged
index 2a3fae16a8..55bf062cff 100755
--- a/discouraged
+++ b/discouraged
@@ -2998,8 +2998,6 @@
 "cbncms" is used by "ubthlem2".
 "cbvexsv" is used by "onfrALTlem1".
 "cbvexsv" is used by "onfrALTlem1VD".
-"cbviinALT" is used by "cbviinvALT".
-"cbviunALT" is used by "cbviunvALT".
 "cbvmptALT" is used by "cbvmptvALT".
 "cbvmptfALT" is used by "cbvmptALT".
 "cbvopab1ALT" is used by "cbvmptfALT".
@@ -6344,8 +6342,6 @@
 "hba1-o" is used by "axc711toc7".
 "hba1-o" is used by "dvelimf-o".
 "hba1-o" is used by "nfa1-o".
-"hbabALT" is used by "bnj1441ALT".
-"hbabALT" is used by "nfsabALT".
 "hbae-o" is used by "aev-o".
 "hbae-o" is used by "dral1-o".
 "hbae-o" is used by "dral2-o".
@@ -9529,13 +9525,6 @@
 "nfa1-o" is used by "ax12eq".
 "nfa1-o" is used by "ax12v2-o".
 "nfa1-o" is used by "axc11n-16".
-"nfabALT" is used by "nfaba1ALT".
-"nfabALT" is used by "nfiinALT".
-"nfabALT" is used by "nfiunALT".
-"nfrexALT" is used by "nfiunALT".
-"nfrexdALT" is used by "nfiundALT".
-"nfrexdALT" is used by "nfrexALT".
-"nfsabALT" is used by "nfabALT".
 "nfsb2ALT" is used by "nfsb4tALT".
 "nfsb4ALT" is used by "sbco2ALT".
 "nfsb4tALT" is used by "nfsb4ALT".
@@ -13825,7 +13814,7 @@ New usage of "bnj1423" is discouraged (1 uses).
 New usage of "bnj1424" is discouraged (2 uses).
 New usage of "bnj1436" is discouraged (12 uses).
 New usage of "bnj1441" is discouraged (0 uses).
-New usage of "bnj1441ALT" is discouraged (0 uses).
+New usage of "bnj1441g" is discouraged (0 uses).
 New usage of "bnj1442" is discouraged (1 uses).
 New usage of "bnj1444" is discouraged (1 uses).
 New usage of "bnj1445" is discouraged (1 uses).
@@ -14075,10 +14064,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 "cbviinALT" is discouraged (1 uses).
-New usage of "cbviinvALT" is discouraged (0 uses).
-New usage of "cbviunALT" is discouraged (1 uses).
-New usage of "cbviunvALT" 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).
@@ -15401,7 +15386,6 @@ New usage of "hatomic" is discouraged (1 uses).
 New usage of "hatomici" is discouraged (6 uses).
 New usage of "hatomistici" is discouraged (1 uses).
 New usage of "hba1-o" is discouraged (8 uses).
-New usage of "hbabALT" is discouraged (2 uses).
 New usage of "hbae-o" is discouraged (4 uses).
 New usage of "hbalg" is discouraged (1 uses).
 New usage of "hbalgVD" is discouraged (0 uses).
@@ -15410,7 +15394,6 @@ New usage of "hbexg" is discouraged (0 uses).
 New usage of "hbexgVD" is discouraged (0 uses).
 New usage of "hbimpg" is discouraged (0 uses).
 New usage of "hbimpgVD" is discouraged (0 uses).
-New usage of "hblemALT" is discouraged (0 uses).
 New usage of "hbnae-o" is discouraged (3 uses).
 New usage of "hbntal" is discouraged (3 uses).
 New usage of "hbra2VD" is discouraged (0 uses).
@@ -16403,22 +16386,14 @@ New usage of "nelne2OLD" is discouraged (0 uses).
 New usage of "nf5rOLD" is discouraged (0 uses).
 New usage of "nf5riOLD" is discouraged (0 uses).
 New usage of "nfa1-o" is discouraged (4 uses).
-New usage of "nfabALT" is discouraged (3 uses).
-New usage of "nfaba1ALT" is discouraged (0 uses).
 New usage of "nfabd2OLD" is discouraged (0 uses).
 New usage of "nfabdOLD" is discouraged (0 uses).
 New usage of "nfceqiOLD" is discouraged (0 uses).
 New usage of "nfcvfOLD" is discouraged (0 uses).
 New usage of "nfequid-o" is discouraged (0 uses).
 New usage of "nfeu1ALT" is discouraged (0 uses).
-New usage of "nfiinALT" is discouraged (0 uses).
-New usage of "nfiunALT" is discouraged (0 uses).
-New usage of "nfiundALT" is discouraged (0 uses).
 New usage of "nfopdALT" is discouraged (0 uses).
-New usage of "nfrexALT" is discouraged (1 uses).
-New usage of "nfrexdALT" is discouraged (2 uses).
 New usage of "nfsab1OLD" is discouraged (0 uses).
-New usage of "nfsabALT" is discouraged (1 uses).
 New usage of "nfsb2ALT" is discouraged (1 uses).
 New usage of "nfsb4ALT" is discouraged (1 uses).
 New usage of "nfsb4tALT" is discouraged (1 uses).
@@ -18230,7 +18205,6 @@ Proof modification of "bj-xpima1snALT" is discouraged (25 steps).
 Proof modification of "bj-xpima2sn" is discouraged (23 steps).
 Proof modification of "bj-xpnzex" is discouraged (71 steps).
 Proof modification of "bj-zfauscl" is discouraged (65 steps).
-Proof modification of "bnj1441ALT" is discouraged (30 steps).
 Proof modification of "brfi1indALT" is discouraged (789 steps).
 Proof modification of "brfvidRP" is discouraged (92 steps).
 Proof modification of "c0exALT" is discouraged (15 steps).
@@ -18244,10 +18218,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 "cbviinALT" is discouraged (64 steps).
-Proof modification of "cbviinvALT" is discouraged (13 steps).
-Proof modification of "cbviunALT" is discouraged (64 steps).
-Proof modification of "cbviunvALT" is discouraged (13 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).
@@ -18816,7 +18786,6 @@ Proof modification of "gsumccatOLD" is discouraged (995 steps).
 Proof modification of "hadcomaOLD" is discouraged (37 steps).
 Proof modification of "hashge3el3dif" is discouraged (229 steps).
 Proof modification of "hba1-o" is discouraged (34 steps).
-Proof modification of "hbabALT" is discouraged (22 steps).
 Proof modification of "hbae-o" is discouraged (85 steps).
 Proof modification of "hbalg" is discouraged (31 steps).
 Proof modification of "hbalgVD" is discouraged (53 steps).
@@ -18825,7 +18794,6 @@ Proof modification of "hbexg" is discouraged (71 steps).
 Proof modification of "hbexgVD" is discouraged (205 steps).
 Proof modification of "hbimpg" is discouraged (88 steps).
 Proof modification of "hbimpgVD" is discouraged (165 steps).
-Proof modification of "hblemALT" is discouraged (33 steps).
 Proof modification of "hbnae-o" is discouraged (11 steps).
 Proof modification of "hbntal" is discouraged (48 steps).
 Proof modification of "hbra2VD" is discouraged (26 steps).
@@ -18996,22 +18964,14 @@ Proof modification of "nelne2OLD" is discouraged (26 steps).
 Proof modification of "nf5rOLD" is discouraged (22 steps).
 Proof modification of "nf5riOLD" is discouraged (13 steps).
 Proof modification of "nfa1-o" is discouraged (8 steps).
-Proof modification of "nfabALT" is discouraged (12 steps).
-Proof modification of "nfaba1ALT" is discouraged (9 steps).
 Proof modification of "nfabd2OLD" is discouraged (75 steps).
 Proof modification of "nfabdOLD" is discouraged (18 steps).
 Proof modification of "nfceqiOLD" is discouraged (21 steps).
 Proof modification of "nfcvfOLD" is discouraged (18 steps).
 Proof modification of "nfequid-o" is discouraged (8 steps).
 Proof modification of "nfeu1ALT" is discouraged (25 steps).
-Proof modification of "nfiinALT" is discouraged (35 steps).
-Proof modification of "nfiunALT" is discouraged (35 steps).
-Proof modification of "nfiundALT" is discouraged (43 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
-Proof modification of "nfrexALT" is discouraged (27 steps).
-Proof modification of "nfrexdALT" is discouraged (34 steps).
 Proof modification of "nfsab1OLD" is discouraged (12 steps).
-Proof modification of "nfsabALT" is discouraged (17 steps).
 Proof modification of "nfsb2ALT" is discouraged (18 steps).
 Proof modification of "nfsb4ALT" is discouraged (23 steps).
 Proof modification of "nfsb4tALT" is discouraged (119 steps).
diff --git a/set.mm b/set.mm
index db797e0183..ad184d1a89 100644
--- a/set.mm
+++ b/set.mm
@@ -25089,6 +25089,7 @@ yield an eliminable and weakly (that is, object-level) conservative
     hbab.1 $e |- ( ph -> A. x ph ) $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
        by NM, 1-Mar-1995.)  Add disjoint variable condition to avoid ~ ax-13 .
+       See ~ hbabg for a less restrictive version requiring more axioms.
        (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 $.
@@ -25096,11 +25097,10 @@ yield an eliminable and weakly (that is, object-level) conservative
 
   ${
     $d x z $.
-    hbabALT.1 $e |- ( ph -> A. x ph ) $.
-    $( Alternate version of ~ hbab , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 1-Mar-1995.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    hbabALT $p |- ( z e. { y | ph } -> A. x z e. { y | ph } ) $=
+    hbabg.1 $e |- ( ph -> A. x ph ) $.
+    $( Bound-variable hypothesis builder for a class abstraction.  (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 $.
   $}
 
@@ -25109,19 +25109,19 @@ yield an eliminable and weakly (that is, object-level) conservative
     nfsab.1 $e |- F/ x ph $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
        by Mario Carneiro, 11-Aug-2016.)  Add disjoint variable condition to
-       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       avoid ~ ax-13 .  See ~ nfsabg for a less restrictive version requiring
+       more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfsab $p |- F/ x z e. { y | ph } $=
       ( cv cab wcel nf5ri hbab nf5i ) DFACGHBABCDABEIJK $.
   $}
 
   ${
     $d x z $.
-    nfsabALT.1 $e |- F/ x ph $.
-    $( Alternate version of ~ nfsab , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfsabALT $p |- F/ x z e. { y | ph } $=
-      ( cv cab wcel nf5ri hbabALT nf5i ) DFACGHBABCDABEIJK $.
+    nfsabg.1 $e |- F/ x ph $.
+    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
+       by Mario Carneiro, 11-Aug-2016.) $)
+    nfsabg $p |- F/ x z e. { y | ph } $=
+      ( cv cab wcel nf5ri hbabg nf5i ) DFACGHBABCDABEIJK $.
   $}
 
 
@@ -26638,8 +26638,9 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
     hblem.1 $e |- ( y e. A -> A. x y e. A ) $.
     $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
        (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.)  Add disjoint variable condition to avoid ~ ax-13 .
-       (Revised by Gino Giotto, 20-Jan-2024.) $)
+       11-Jul-2011.)  Add disjoint variable condition to avoid ~ ax-13 .  See
+       ~ hblemg for a less restrictive version requiring more axioms.  (Revised
+       by Gino Giotto, 20-Jan-2024.) $)
     hblem $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsbw clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAE
       JBCDKZOPAQLM $.
@@ -26647,11 +26648,11 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
 
   ${
     $d y A $.  $d x z $.
-    hblemALT.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Alternate version of ~ hblem , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    hblemALT $p |- ( z e. A -> A. x z e. A ) $=
+    hblemg.1 $e |- ( y e. A -> A. x y e. A ) $.
+    $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
+       (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 $.
   $}
@@ -27067,35 +27068,35 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
     nfab.1 $e |- F/ x ph $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
        by Mario Carneiro, 11-Aug-2016.)  Add disjoint variable condition to
-       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       avoid ~ ax-13 .  See ~ nfabg for a less restrictive version requiring
+       more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfab $p |- F/_ x { y | ph } $=
       ( vz cab nfsab nfci ) BEACFABCEDGH $.
   $}
 
   ${
     $d x z $.  $d y z $.  $d z ph $.
-    nfabALT.1 $e |- F/ x ph $.
-    $( Alternate version of ~ nfab , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 11-Aug-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfabALT $p |- F/_ x { y | ph } $=
-      ( vz cab nfsabALT nfci ) BEACFABCEDGH $.
+    nfabg.1 $e |- F/ x ph $.
+    $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
+       by Mario Carneiro, 11-Aug-2016.) $)
+    nfabg $p |- F/_ x { y | ph } $=
+      ( vz cab nfsabg nfci ) BEACFABCEDGH $.
   $}
 
   ${
     $d x y $.
     $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
        by Mario Carneiro, 14-Oct-2016.)  Add disjoint variable condition to
-       avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       avoid ~ ax-13 .  See ~ nfaba1g for a less restrictive version requiring
+       more axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfaba1 $p |- F/_ x { y | A. x ph } $=
       ( wal nfa1 nfab ) ABDBCABEF $.
   $}
 
-  $( Alternate version of ~ nfaba1 , with no dv conditions, but requiring
-     ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.)
-     (Proof modification is discouraged.)  (New usage is discouraged.) $)
-  nfaba1ALT $p |- F/_ x { y | A. x ph } $=
-    ( wal nfa1 nfabALT ) ABDBCABEF $.
+  $( Bound-variable hypothesis builder for a class abstraction.  (Contributed
+     by Mario Carneiro, 14-Oct-2016.) $)
+  nfaba1g $p |- F/_ x { y | A. x ph } $=
+    ( wal nfa1 nfabg ) ABDBCABEF $.
 
   ${
     $d x y $.  $d y A $.  $d y B $.  $d y ph $.
@@ -29794,7 +29795,8 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     nfrexd.2 $e |- ( ph -> F/_ x A ) $.
     nfrexd.3 $e |- ( ph -> F/ x ps ) $.
     $( Deduction version of ~ nfrex .  (Contributed by Mario Carneiro,
-       14-Oct-2016.)  Add disjoint variable condition to avoid ~ ax-13 .
+       14-Oct-2016.)  Add disjoint variable condition to avoid ~ ax-13 .  See
+       ~ nfrexdg for a less restrictive version requiring more axioms.
        (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfrexd $p |- ( ph -> F/ x E. y e. A ps ) $=
       ( wrex wn wral dfrex2 nfnd nfraldw nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGA
@@ -29802,13 +29804,12 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
   $}
 
   ${
-    nfrexdALT.1 $e |- F/ y ph $.
-    nfrexdALT.2 $e |- ( ph -> F/_ x A ) $.
-    nfrexdALT.3 $e |- ( ph -> F/ x ps ) $.
-    $( Alternate version of ~ nfrexd , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 14-Oct-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfrexdALT $p |- ( ph -> F/ x E. y e. A ps ) $=
+    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.) $)
+    nfrexdg $p |- ( ph -> F/ x E. y e. A ps ) $=
       ( wrex wn wral dfrex2 nfnd nfrald nfxfrd ) BDEIBJZDEKZJACBDELAQCAPCDEFGAB
       CHMNMO $.
   $}
@@ -29820,7 +29821,8 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     $( 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.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       disjoint variable condition to avoid ~ ax-13 .  See ~ nfrexg for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
        20-Jan-2024.) $)
     nfrex $p |- F/ x E. y e. A ph $=
       ( wrex wnf wtru nftru wnfc a1i nfrexd mptru ) ACDGBHIABCDCJBDKIELABHIFLMN
@@ -29828,15 +29830,14 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
   $}
 
   ${
-    nfrexALT.1 $e |- F/_ x A $.
-    nfrexALT.2 $e |- F/ x ph $.
-    $( Alternate version of ~ nfrex , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 1-Sep-1999.)  (Revised by Mario Carneiro,
-       7-Oct-2016.)  (Proof shortened by Wolf Lammen, 30-Dec-2019.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfrexALT $p |- F/ x E. y e. A ph $=
-      ( wrex wnf wtru nftru wnfc a1i nfrexdALT mptru ) ACDGBHIABCDCJBDKIELABHIF
-      LMN $.
+    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.) $)
+    nfrexg $p |- F/ x E. y e. A ph $=
+      ( wrex wnf wtru nftru wnfc a1i nfrexdg mptru ) ACDGBHIABCDCJBDKIELABHIFLM
+      N $.
   $}
 
   ${
@@ -44829,14 +44830,17 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     nfiun.2 $e |- F/_ y B $.
     $( Bound-variable hypothesis builder for indexed union.  (Contributed by
        Mario Carneiro, 25-Jan-2014.)  Add disjoint variable condition to avoid
-       ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       ~ ax-13 .  See ~ nfiung for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfiun $p |- F/_ y U_ x e. A B $=
       ( vz ciun cv wcel wrex cab df-iun nfcri nfrex nfab nfcxfr ) BACDHGIDJZACK
       ZGLAGCDMSBGRBACEBGDFNOPQ $.
 
     $( Bound-variable hypothesis builder for indexed intersection.
        (Contributed by Mario Carneiro, 25-Jan-2014.)  Add disjoint variable
-       condition to avoid ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       condition to avoid ~ ax-13 .  See ~ nfiing for a less restrictive
+       version requiring more axioms.  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
     nfiin $p |- F/_ y |^|_ x e. A B $=
       ( vz ciin cv wcel wral cab df-iin nfcri nfralw nfab nfcxfr ) BACDHGIDJZAC
       KZGLAGCDMSBGRBACEBGDFNOPQ $.
@@ -44844,21 +44848,19 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
 
   ${
     $d z A $.  $d z B $.  $d x z $.  $d y z $.
-    nfiunALT.1 $e |- F/_ y A $.
-    nfiunALT.2 $e |- F/_ y B $.
-    $( Alternate version of ~ nfiun , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfiunALT $p |- F/_ y U_ x e. A B $=
-      ( vz ciun cv wcel wrex cab df-iun nfcri nfrexALT nfabALT nfcxfr ) BACDHGI
-      DJZACKZGLAGCDMSBGRBACEBGDFNOPQ $.
+    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.) $)
+    nfiung $p |- F/_ y U_ x e. A B $=
+      ( vz ciun cv wcel wrex cab df-iun nfcri nfrexg nfabg nfcxfr ) BACDHGIDJZA
+      CKZGLAGCDMSBGRBACEBGDFNOPQ $.
 
-    $( Alternate version of ~ nfiin , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Mario Carneiro, 25-Jan-2014.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfiinALT $p |- F/_ y |^|_ x e. A B $=
-      ( vz ciin cv wcel wral cab df-iin nfcri nfral nfabALT nfcxfr ) BACDHGIDJZ
-      ACKZGLAGCDMSBGRBACEBGDFNOPQ $.
+    $( Bound-variable hypothesis builder for indexed intersection.
+       (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 $.
   $}
 
   ${
@@ -44955,7 +44957,8 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $( 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.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       disjoint variable condition to avoid ~ ax-13 .  See ~ cbviung for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
        20-Jan-2024.) $)
     cbviun $p |- U_ x e. A B = U_ y e. A C $=
       ( vz cv wcel wrex cab ciun nfcri weq eleq2d cbvrexw abbii df-iun 3eqtr4i
@@ -44964,7 +44967,8 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
 
     $( Change bound variables in an indexed intersection.  (Contributed by Jeff
        Hankins, 26-Aug-2009.)  (Revised by Mario Carneiro, 14-Oct-2016.)  Add
-       disjoint variable condition to avoid ~ ax-13 .  (Revised by Gino Giotto,
+       disjoint variable condition to avoid ~ ax-13 .  See ~ cbviing for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
        20-Jan-2024.) $)
     cbviin $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( vz cv wcel wral cab ciin nfcri weq eleq2d cbvralw abbii df-iin 3eqtr4i
@@ -44974,23 +44978,20 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
 
   ${
     $d z y A $.  $d z x A $.  $d z B $.  $d z C $.
-    cbviunALT.1 $e |- F/_ y B $.
-    cbviunALT.2 $e |- F/_ x C $.
-    cbviunALT.3 $e |- ( x = y -> B = C ) $.
-    $( Alternate version of ~ cbviun , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 26-Mar-2006.)  (Revised by Andrew Salmon,
-       25-Jul-2011.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cbviunALT $p |- U_ x e. A B = U_ y e. A C $=
+    cbviung.1 $e |- F/_ y B $.
+    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.) $)
+    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 $.
 
-    $( Alternate version of ~ cbviin , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.)  (Revised by
-       Mario Carneiro, 14-Oct-2016.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cbviinALT $p |- |^|_ x e. A B = |^|_ y e. A C $=
+    $( Change bound variables in an indexed intersection.  (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
       TUA $.
@@ -45002,31 +45003,32 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $( 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.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
 
     $( Change bound variables in an indexed intersection.  (Contributed by Jeff
-       Hankins, 26-Aug-2009.) $)
+       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 $.
   $}
 
   ${
     $d x A $.  $d y A $.  $d y B $.  $d x C $.
-    cbviunvALT.1 $e |- ( x = y -> B = C ) $.
-    $( Alternate version of ~ cbviunv , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.)  (Revised by Gino Giotto,
-       20-Jan-2024.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cbviunvALT $p |- U_ x e. A B = U_ y e. A C $=
-      ( nfcv cbviunALT ) ABCDEBDGAEGFH $.
+    cbviunvg.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.) $)
+    cbviunvg $p |- U_ x e. A B = U_ y e. A C $=
+      ( nfcv cbviung ) ABCDEBDGAEGFH $.
 
-    $( Alternate version of ~ cbviinv , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    cbviinvALT $p |- |^|_ x e. A B = |^|_ y e. A C $=
-      ( nfcv cbviinALT ) ABCDEBDGAEGFH $.
+    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
+       Hankins, 26-Aug-2009.) $)
+    cbviinvg $p |- |^|_ x e. A B = |^|_ y e. A C $=
+      ( nfcv cbviing ) ABCDEBDGAEGFH $.
   $}
 
   ${
@@ -497102,7 +497104,8 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
     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 .
+       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
@@ -497111,14 +497114,13 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a
 
   ${
     $d y z $.
-    bnj1441ALT.1 $e |- ( x e. A -> A. y x e. A ) $.
-    bnj1441ALT.2 $e |- ( ph -> A. y ph ) $.
-    $( Alternate version of ~ bnj1441 , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    bnj1441ALT $p |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) $=
-      ( crab cv wcel wa cab df-rab hban hbabALT hbxfreq ) CDABEHBIEJZAKZBLABEMR
-      CBDQACFGNOP $.
+    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.) $)
+    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 $.
   $}
 
   ${
@@ -752144,7 +752146,8 @@ coordinates of the intersection points of a (nondegenerate) line and a
     nfiund.3 $e |- ( ph -> F/_ y B ) $.
     $( Bound-variable hypothesis builder for indexed union.  (Contributed by
        Emmett Weisz, 6-Dec-2019.)  Add disjoint variable condition to avoid
-       ~ ax-13 .  (Revised by Gino Giotto, 20-Jan-2024.) $)
+       ~ ax-13 .  See ~ nfiundg for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     nfiund $p |- ( ph -> F/_ y U_ x e. A B ) $=
       ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexd nfabdw nfcxfrd ) ACBDE
       JIKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.
@@ -752152,15 +752155,14 @@ coordinates of the intersection points of a (nondegenerate) line and a
 
   ${
     $d z ph $.  $d z A $.  $d z B $.  $d z x $.  $d z y $.
-    nfiundALT.1 $e |- F/ x ph $.
-    nfiundALT.2 $e |- ( ph -> F/_ y A ) $.
-    nfiundALT.3 $e |- ( ph -> F/_ y B ) $.
-    $( Alternate version of ~ nfiund , with less dv conditions, but requiring
-       ~ ax-13 .  (Contributed by Emmett Weisz, 6-Dec-2019.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfiundALT $p |- ( ph -> F/_ y U_ x e. A B ) $=
-      ( vz ciun cv wcel wrex cab df-iun nfv nfcrd nfrexdALT nfabd nfcxfrd ) ACB
-      DEJIKELZBDMZINBIDEOAUBCIAIPAUACBDFGACIEHQRST $.
+    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.) $)
+    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 d6fa64fa7f9a7cfcb51c3b297106f286e3aae91d Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Tue, 23 Jan 2024 00:31:51 +0100
Subject: [PATCH 5/6] comment correction

---
 set.mm | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/set.mm b/set.mm
index ad184d1a89..2da2dc4f65 100644
--- a/set.mm
+++ b/set.mm
@@ -26636,11 +26636,11 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d y A $.  $d x z $.  $d x y $.
     hblem.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
-       (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.)  Add disjoint variable condition to avoid ~ ax-13 .  See
-       ~ hblemg for a less restrictive version requiring more axioms.  (Revised
-       by Gino Giotto, 20-Jan-2024.) $)
+    $( Change the free variable of a hypothesis builder.  (Contributed by NM,
+       21-Jun-1993.)  (Revised by Andrew Salmon, 11-Jul-2011.)  Add disjoint
+       variable condition to avoid ~ ax-13 .  See ~ hblemg for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
     hblem $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsbw clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAE
       JBCDKZOPAQLM $.
@@ -26649,9 +26649,8 @@ 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.  Lemma for ~ nfcrii .
-       (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.) $)
+    $( Change the free variable of a hypothesis builder.  (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 $.

From a5d477778bdd55a31866a8a669d79413982c2ef7 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Wed, 24 Jan 2024 19:03:41 +0100
Subject: [PATCH 6/6] updated changes-set.txt

---
 changes-set.txt | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/changes-set.txt b/changes-set.txt
index c4e936e9d0..ba8ef95a24 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -79,6 +79,21 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+20-Jan-24 nfiund    nfiundg
+20-Jan-24 bnj1441   bnj1441g
+20-Jan-24 cbviinv   cbviinvg
+20-Jan-24 cbviunv   cbviunvg
+20-Jan-24 cbviin    cbviing
+20-Jan-24 cbviun    cbviung
+20-Jan-24 nfiin     nfiing
+20-Jan-24 nfiun     nfiung
+20-Jan-24 nfrex     nfrexg
+20-Jan-24 nfrexd    nfrexdg
+20-Jan-24 nfaba1    nfaba1g
+20-Jan-24 nfab      nfabg
+20-Jan-24 hblem     hblemg
+20-Jan-24 nfsab     nfsabg
+20-Jan-24 hbab      hbabg 
 17-Jan-24 mteqand   [same]      moved from SN's mathbox to main set.mm
 15-Jan-24 sseqtr4d  sseqtrrd
 14-Jan-24 sseqtr4i  sseqtrri