eqab -> eqabb (#4676)

* eqabw -> eqabbw

* eqab -> eqabb

* delete outdated OLD

* abbi -> abbib in nf.mm

* eqab -> eqabb in nf.mm

* update eqab reference in comment in nf.mm

* update mmset.raw.html

* shorten eqabr

* typo

* rm duplicated line

* eqabc -> eqabbc

* eqabbc -> eqabcb

changes-set.txt

@@ -143,9 +143,9 @@ Date      Old       New         Notes
 15-Feb-25 abeq1i    eqabci
 15-Feb-25 abeq2i    eqabi
 15-Feb-25 abeq2d    eqabd
-15-Feb-25 abeq2w    eqabw
-15-Feb-25 abeq1     eqabc       Commuted form of eqab
-15-Feb-25 abeq2     eqab        Basic closed form
+15-Feb-25 abeq2w    eqabbw
+15-Feb-25 abeq1     eqabbc      Commuted form of eqabb
+15-Feb-25 abeq2     eqabb       Basic closed form
 14-Feb-25 ---       ---         Moved surreal negation theorems
                                 from SF's mathbox to main set.mm
 14-Feb-25 grpinvcld ---         Moved from SN's mathbox to main set.mm

discouraged

@@ -10397,7 +10397,6 @@
 "nfsb2" is used by "sb9".
 "nfsb2" is used by "sbco3".
 "nfsb2" is used by "wl-nfs1t".
-"nfsb4" is used by "nfsbOLD".
 "nfsb4" is used by "sbco2".
 "nfsb4t" is used by "nfsb4".
 "nfsb4t" is used by "nfsbd".
@@ -16579,7 +16578,7 @@ New usage of "epweonALT" is discouraged (0 uses).
 New usage of "eq0ALT" is discouraged (0 uses).
 New usage of "eq0OLDOLD" is discouraged (0 uses).
 New usage of "eq0rdvALT" is discouraged (0 uses).
-New usage of "eqabOLD" is discouraged (0 uses).
+New usage of "eqabbOLD" is discouraged (0 uses).
 New usage of "eqeq12OLD" is discouraged (1 uses).
 New usage of "eqeq12dOLD" is discouraged (1 uses).
 New usage of "eqeq1dALT" is discouraged (0 uses).
@@ -17999,9 +17998,8 @@ New usage of "nfs1" is discouraged (2 uses).
 New usage of "nfsabg" is discouraged (1 uses).
 New usage of "nfsb" is discouraged (17 uses).
 New usage of "nfsb2" is discouraged (4 uses).
-New usage of "nfsb4" is discouraged (2 uses).
+New usage of "nfsb4" is discouraged (1 uses).
 New usage of "nfsb4t" is discouraged (2 uses).
-New usage of "nfsbOLD" is discouraged (0 uses).
 New usage of "nfsbc" is discouraged (4 uses).
 New usage of "nfsbcd" is discouraged (3 uses).
 New usage of "nfsbd" is discouraged (3 uses).
@@ -20477,7 +20475,7 @@ Proof modification of "epweonALT" is discouraged (86 steps).
 Proof modification of "eq0ALT" is discouraged (31 steps).
 Proof modification of "eq0OLDOLD" is discouraged (6 steps).
 Proof modification of "eq0rdvALT" is discouraged (25 steps).
-Proof modification of "eqabOLD" is discouraged (47 steps).
+Proof modification of "eqabbOLD" is discouraged (47 steps).
 Proof modification of "eqeq12OLD" is discouraged (24 steps).
 Proof modification of "eqeq12dOLD" is discouraged (22 steps).
 Proof modification of "eqeq1dALT" is discouraged (62 steps).
@@ -21000,7 +20998,6 @@ Proof modification of "nfraldwOLD" is discouraged (41 steps).
 Proof modification of "nfralwOLD" is discouraged (27 steps).
 Proof modification of "nfreuwOLD" is discouraged (56 steps).
 Proof modification of "nfrmowOLD" is discouraged (55 steps).
-Proof modification of "nfsbOLD" is discouraged (23 steps).
 Proof modification of "nfsbvOLD" is discouraged (47 steps).
 Proof modification of "nfunidALT" is discouraged (33 steps).
 Proof modification of "nfunidALT2" is discouraged (49 steps).

mmset.raw.html

@@ -2022,7 +2022,7 @@
 may be the same) as long as they don't conflict with any distinct variable
 requirements imposed on ` A ` and ` B ` .  We then would
 follow the procedure of the above example.  The description of theorem
-~ eqab goes into more detail and gives some
+~ eqabb goes into more detail and gives some
 actual database examples where this translation takes place.
 </P>
 
@@ -2229,7 +2229,7 @@
 <LI>Commutative law for union ~ uncom</LI>
 
 <LI>A basic relationship between class and wff
-variables ~ eqab</LI>
+variables ~ eqabb</LI>
 
 <LI>Two ways of saying &quot;is a set&quot; ~ isset</LI>