Revision for Base

* Usage of df-base discouraged
* some *ndxn* theorems reordered
* ~basendxltdsndxn renamed ~basendxltdsndx
* ~slotsbaseefdif  renamed ~basendxnedgfndx
* proof of ~symgvalstruct shortened
* proofs of ~rlmscaf , ~ply1tmcl, ~ply1scltm, ~ply1sclf, ~ply1scl0, ~ply1scl1   revised

changes-set.txt

@@ -95,6 +95,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 7-Nov-24 slotsbaseefdif basendxnedgfndx
 24-Oct-24 ---       ---         well-founded recursion theorems moved
                                 from SF's mathbox to main set.mm
 22-Oct-24 ---       ---         well-founded induction theorems moved

discouraged

@@ -1673,7 +1673,7 @@
 "basendx" is used by "2strstr".
 "basendx" is used by "2strstr1OLD".
 "basendx" is used by "baseltedgf".
-"basendx" is used by "basendxltdsndxn".
+"basendx" is used by "basendxltdsndx".
 "basendx" is used by "basendxltplendx".
 "basendx" is used by "basendxltplusgndx".
 "basendx" is used by "basendxlttsetndx".
@@ -4579,6 +4579,38 @@
 "df-at" is used by "atssch".
 "df-at" is used by "ela".
 "df-ba" is used by "bafval".
+"df-base" is used by "1strwunOLD".
+"df-base" is used by "baseid".
+"df-base" is used by "baseltedgfOLD".
+"df-base" is used by "basendx".
+"df-base" is used by "basendxnmulrndxOLD".
+"df-base" is used by "basendxnnOLD".
+"df-base" is used by "basendxnplusgndxOLD".
+"df-base" is used by "baseval".
+"df-base" is used by "bj-endbase".
+"df-base" is used by "catcfucclOLD".
+"df-base" is used by "catcoppcclOLD".
+"df-base" is used by "catcxpcclOLD".
+"df-base" is used by "estrreslem1OLD".
+"df-base" is used by "hlhilsbaseOLD".
+"df-base" is used by "mgpbasOLD".
+"df-base" is used by "mnringbasedOLD".
+"df-base" is used by "oppgbasOLD".
+"df-base" is used by "opprbasOLD".
+"df-base" is used by "opsrbasOLD".
+"df-base" is used by "ressval3dOLD".
+"df-base" is used by "resvbasOLD".
+"df-base" is used by "rmodislmodOLD".
+"df-base" is used by "slotsbhcdifOLD".
+"df-base" is used by "srabaseOLD".
+"df-base" is used by "symgvalstructOLD".
+"df-base" is used by "tngbasOLD".
+"df-base" is used by "ttgbasOLD".
+"df-base" is used by "wunfuncOLD".
+"df-base" is used by "wunnatOLD".
+"df-base" is used by "wunressOLD".
+"df-base" is used by "zlmbasOLD".
+"df-base" is used by "znbas2OLD".
 "df-bdop" is used by "elbdop".
 "df-bdop" is used by "hhbloi".
 "df-bj-1upl" is used by "bj-1upleq".
@@ -15547,6 +15579,7 @@ New usage of "df-aj" is discouraged (1 uses).
 New usage of "df-ass" is discouraged (1 uses).
 New usage of "df-at" is discouraged (2 uses).
 New usage of "df-ba" is discouraged (1 uses).
+New usage of "df-base" is discouraged (32 uses).
 New usage of "df-bdop" is discouraged (2 uses).
 New usage of "df-bj-1upl" is discouraged (6 uses).
 New usage of "df-bj-2upl" is discouraged (6 uses).
@@ -18894,6 +18927,7 @@ New usage of "syl5imp" is discouraged (0 uses).
 New usage of "syl5impVD" is discouraged (0 uses).
 New usage of "symgbasexOLD" is discouraged (0 uses).
 New usage of "symgsubmefmndALT" is discouraged (0 uses).
+New usage of "symgvalstructOLD" is discouraged (0 uses).
 New usage of "tarski-bernays-ax2" is discouraged (0 uses).
 New usage of "tb-ax1" is discouraged (3 uses).
 New usage of "tb-ax2" is discouraged (1 uses).
@@ -20752,6 +20786,7 @@ Proof modification of "syl5imp" is discouraged (23 steps).
 Proof modification of "syl5impVD" is discouraged (57 steps).
 Proof modification of "symgbasexOLD" is discouraged (24 steps).
 Proof modification of "symgsubmefmndALT" is discouraged (129 steps).
+Proof modification of "symgvalstructOLD" is discouraged (651 steps).
 Proof modification of "symrefref3" is discouraged (75 steps).
 Proof modification of "tarski-bernays-ax2" is discouraged (557 steps).
 Proof modification of "tb-ax1" is discouraged (4 steps).