Follow up of # 4648

changes-set.txt

@@ -85,6 +85,14 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+15-Feb-25 abeq2f    eqabf
+15-Feb-25 rabeq2i   reqabi
+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
 14-Feb-25 ---       ---         Moved surreal negation theorems
                                 from SF's mathbox to main set.mm
 10-Feb-25 ---       ---         Moved surreal addition theorems

discouraged

@@ -14414,7 +14414,6 @@ New usage of "aaanOLD" is discouraged (0 uses).
 New usage of "ab0ALT" is discouraged (0 uses).
 New usage of "ab0OLD" is discouraged (0 uses).
 New usage of "ab0orvALT" is discouraged (0 uses).
-New usage of "abeq2OLD" is discouraged (0 uses).
 New usage of "abfOLD" is discouraged (0 uses).
 New usage of "ablo32" is discouraged (4 uses).
 New usage of "ablo4" is discouraged (3 uses).
@@ -16587,6 +16586,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 "eqeq12OLD" is discouraged (1 uses).
 New usage of "eqeq12dOLD" is discouraged (1 uses).
 New usage of "eqeq1dALT" is discouraged (0 uses).
@@ -19721,7 +19721,6 @@ Proof modification of "aaanOLD" is discouraged (38 steps).
 Proof modification of "ab0ALT" is discouraged (33 steps).
 Proof modification of "ab0OLD" is discouraged (146 steps).
 Proof modification of "ab0orvALT" is discouraged (19 steps).
-Proof modification of "abeq2OLD" is discouraged (47 steps).
 Proof modification of "abfOLD" is discouraged (13 steps).
 Proof modification of "abn0OLD" is discouraged (28 steps).
 Proof modification of "abrexexgOLD" is discouraged (43 steps).
@@ -20486,6 +20485,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 "eqeq12OLD" is discouraged (24 steps).
 Proof modification of "eqeq12dOLD" is discouraged (22 steps).
 Proof modification of "eqeq1dALT" is discouraged (62 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
-~ abeq2 goes into more detail and gives some
+~ eqab 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 ~ abeq2</LI>
+variables ~ eqab</LI>
 
 <LI>Two ways of saying &quot;is a set&quot; ~ isset</LI>