Follow up of # 4648 (metamath#4654)

* abeq2 -> eqab * abeq1 -> eqabc * abeq2impr -> eqab1r * abeq2w -> eqabw * abeq2d -> eqabd * abeq2i -> eqabi * abeq1i -> eqabci * rabeq2i -> reqabi * abeq2f -> eqabf * discouraged * update nf.mm * update mmset.raw.html * update nf.mm * nf.mm again * Update changes-set.txt Co-authored-by: Benoit <[email protected]> * Update changes-set.txt Co-authored-by: Benoit <[email protected]> * rename merged rabeq2i * fix merge problem * eqab1r -> eqabr * fix eqab1r in $j tag --------- Co-authored-by: Benoit <[email protected]>
jkingdon · Feb 16, 2025 · 5ae7434 · 5ae7434
1 parent 03407c6
commit 5ae7434
Show file tree

Hide file tree

Showing 5 changed files with 2,548 additions and 2,539 deletions.
diff --git a/changes-set.txt b/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

diff --git a/discouraged b/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).

diff --git a/mmset.raw.html b/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>