diff --git a/discouraged b/discouraged
index 59d1620e4b..26f075702b 100644
--- a/discouraged
+++ b/discouraged
@@ -9889,8 +9889,6 @@
 "mndtcval" is used by "mndtchom".
 "moexex" is used by "2moswap".
 "moexex" is used by "moexexv".
-"mptmpoopabbrdOLDOLD" is used by "mptmpoopabovdOLD".
-"mptmpoopabovdOLD" is used by "wksonproplemOLD".
 "mpv" is used by "mulcompr".
 "mulassnq" is used by "1idpr".
 "mulassnq" is used by "addclprlem2".
@@ -11560,7 +11558,6 @@
 "onsetreclem3" is used by "onsetrec".
 "opabid" is used by "brabidga".
 "opabid" is used by "ssopab2b".
-"opabresex2d" is used by "mptmpoopabbrdOLDOLD".
 "opelcn" is used by "axicn".
 "opelreal" is used by "ax1cn".
 "opelreal" is used by "axaddrcl".
@@ -14249,10 +14246,8 @@ New usage of "ablogrpo" is discouraged (24 uses).
 New usage of "ablomuldiv" is discouraged (3 uses).
 New usage of "ablonncan" is discouraged (1 uses).
 New usage of "ablonnncan1" is discouraged (1 uses).
-New usage of "abrexexgOLD" is discouraged (0 uses).
 New usage of "abscncfALT" is discouraged (0 uses).
 New usage of "abshicom" is discouraged (1 uses).
-New usage of "abssdvOLD" is discouraged (0 uses).
 New usage of "abvALT" is discouraged (0 uses).
 New usage of "ac2" is discouraged (1 uses).
 New usage of "ac3" is discouraged (1 uses).
@@ -15622,7 +15617,6 @@ New usage of "conventions-comments" is discouraged (0 uses).
 New usage of "conventions-labels" is discouraged (0 uses).
 New usage of "copsexg" is discouraged (1 uses).
 New usage of "cotrgOLD" is discouraged (0 uses).
-New usage of "cotrgOLDOLD" is discouraged (0 uses).
 New usage of "counop" is discouraged (0 uses).
 New usage of "crhmsubcALTV" is discouraged (1 uses).
 New usage of "cringcALTV" is discouraged (9 uses).
@@ -15867,14 +15861,10 @@ New usage of "dfdif3OLD" is discouraged (0 uses).
 New usage of "dfeu" is discouraged (0 uses).
 New usage of "dffr2ALT" is discouraged (0 uses).
 New usage of "dffun2OLD" is discouraged (0 uses).
-New usage of "dffun2OLDOLD" is discouraged (0 uses).
-New usage of "dffun3OLD" is discouraged (0 uses).
-New usage of "dffun6OLD" is discouraged (0 uses).
 New usage of "dfhnorm2" is discouraged (3 uses).
 New usage of "dfid2" is discouraged (0 uses).
 New usage of "dfid3" is discouraged (0 uses).
 New usage of "dfiop2" is discouraged (3 uses).
-New usage of "dfiun2gOLD" is discouraged (0 uses).
 New usage of "dfmo" is discouraged (0 uses).
 New usage of "dfpjop" is discouraged (4 uses).
 New usage of "dfsb1" is discouraged (3 uses).
@@ -15941,7 +15931,6 @@ New usage of "dif1enOLD" is discouraged (0 uses).
 New usage of "dif1enlemOLD" is discouraged (2 uses).
 New usage of "dif1ennnALT" is discouraged (0 uses).
 New usage of "difidALT" is discouraged (0 uses).
-New usage of "difopabOLD" is discouraged (0 uses).
 New usage of "dih0bN" is discouraged (0 uses).
 New usage of "dih0vbN" is discouraged (0 uses).
 New usage of "dih2dimbALTN" is discouraged (0 uses).
@@ -16052,7 +16041,6 @@ New usage of "dmmulpi" is discouraged (6 uses).
 New usage of "dmmulsr" is discouraged (3 uses).
 New usage of "dmplp" is discouraged (9 uses).
 New usage of "dmrecnq" is discouraged (2 uses).
-New usage of "dmxpOLD" is discouraged (0 uses).
 New usage of "doca2N" is discouraged (1 uses).
 New usage of "doca3N" is discouraged (1 uses).
 New usage of "docaclN" is discouraged (2 uses).
@@ -16354,8 +16342,6 @@ New usage of "elnlfn2" is discouraged (2 uses).
 New usage of "elnoOLD" is discouraged (0 uses).
 New usage of "elnp" is discouraged (5 uses).
 New usage of "elnpi" is discouraged (4 uses).
-New usage of "elopabrOLD" is discouraged (0 uses).
-New usage of "elopaelxpOLD" is discouraged (0 uses).
 New usage of "elovmporab1" is discouraged (0 uses).
 New usage of "elpaddatiN" is discouraged (2 uses).
 New usage of "elpaddatriN" is discouraged (0 uses).
@@ -16556,13 +16542,10 @@ New usage of "funcringcsetclem8ALTV" is discouraged (1 uses).
 New usage of "funcringcsetclem9ALTV" is discouraged (1 uses).
 New usage of "funcrngcsetcALT" is discouraged (0 uses).
 New usage of "fundcmpsurinjALT" is discouraged (0 uses).
-New usage of "funimaexgOLD" is discouraged (0 uses).
-New usage of "funmoOLD" is discouraged (0 uses).
 New usage of "funop" is discouraged (2 uses).
 New usage of "funopg" is discouraged (0 uses).
 New usage of "funopsn" is discouraged (2 uses).
 New usage of "fvimacnvALT" is discouraged (0 uses).
-New usage of "fvmptopabOLD" is discouraged (0 uses).
 New usage of "fvn0fvelrnOLD" is discouraged (0 uses).
 New usage of "fvprcALT" is discouraged (0 uses).
 New usage of "fvssunirnOLD" is discouraged (0 uses).
@@ -17208,7 +17191,6 @@ New usage of "ipz" is discouraged (1 uses).
 New usage of "isablo" is discouraged (3 uses).
 New usage of "isabloi" is discouraged (3 uses).
 New usage of "isanmbfmOLD" is discouraged (0 uses).
-New usage of "isarep1OLD" is discouraged (0 uses).
 New usage of "isass" is discouraged (1 uses).
 New usage of "isblo" is discouraged (5 uses).
 New usage of "isblo2" is discouraged (1 uses).
@@ -17289,7 +17271,6 @@ New usage of "iunconnALT" is discouraged (0 uses).
 New usage of "iunconnlem2" is discouraged (1 uses).
 New usage of "iuneq12dOLD" is discouraged (0 uses).
 New usage of "iunidOLD" is discouraged (0 uses).
-New usage of "iunopabOLD" is discouraged (0 uses).
 New usage of "ivthALT" is discouraged (0 uses).
 New usage of "jaoded" is discouraged (1 uses).
 New usage of "joincomALT" is discouraged (1 uses).
@@ -17679,8 +17660,6 @@ New usage of "moexex" is discouraged (2 uses).
 New usage of "moexexv" is discouraged (0 uses).
 New usage of "mof0ALT" is discouraged (0 uses).
 New usage of "mptmpoopabbrdOLD" is discouraged (0 uses).
-New usage of "mptmpoopabbrdOLDOLD" is discouraged (1 uses).
-New usage of "mptmpoopabovdOLD" is discouraged (1 uses).
 New usage of "mptssALT" is discouraged (0 uses).
 New usage of "mpv" is discouraged (1 uses).
 New usage of "mrelatglbALT" is discouraged (0 uses).
@@ -17777,7 +17756,6 @@ New usage of "nfra2" is discouraged (1 uses).
 New usage of "nfrab" is discouraged (2 uses).
 New usage of "nfral" is discouraged (5 uses).
 New usage of "nfrald" is discouraged (2 uses).
-New usage of "nfralwOLD" is discouraged (0 uses).
 New usage of "nfreu" is discouraged (0 uses).
 New usage of "nfreud" is discouraged (1 uses).
 New usage of "nfrex" is discouraged (1 uses).
@@ -18115,7 +18093,6 @@ New usage of "onsetreclem3" is discouraged (1 uses).
 New usage of "ontrciOLD" is discouraged (0 uses).
 New usage of "onuniorsuciOLD" is discouraged (0 uses).
 New usage of "opabid" is discouraged (2 uses).
-New usage of "opabresex2d" is discouraged (1 uses).
 New usage of "opelcn" is discouraged (1 uses).
 New usage of "opelopab4" is discouraged (0 uses).
 New usage of "opelreal" is discouraged (8 uses).
@@ -18477,7 +18454,6 @@ New usage of "qlaxr3i" is discouraged (0 uses).
 New usage of "qlaxr4i" is discouraged (0 uses).
 New usage of "qlaxr5i" is discouraged (0 uses).
 New usage of "quoremnn0ALT" is discouraged (0 uses).
-New usage of "r19.21vOLD" is discouraged (0 uses).
 New usage of "r19.29OLD" is discouraged (0 uses).
 New usage of "r19.29rOLD" is discouraged (0 uses).
 New usage of "r19.35OLD" is discouraged (0 uses).
@@ -18575,7 +18551,6 @@ New usage of "rexeqbidvvOLD" is discouraged (0 uses).
 New usage of "rexeqfOLD" is discouraged (0 uses).
 New usage of "reximaOLD" is discouraged (0 uses).
 New usage of "rexlimddvcbv" is discouraged (0 uses).
-New usage of "rexlimivOLD" is discouraged (0 uses).
 New usage of "rexlimivaOLD" is discouraged (0 uses).
 New usage of "rexlimivwOLD" is discouraged (0 uses).
 New usage of "rexor" is discouraged (0 uses).
@@ -18762,7 +18737,6 @@ New usage of "sbtr" is discouraged (0 uses).
 New usage of "sbtrt" is discouraged (1 uses).
 New usage of "scandx" is discouraged (12 uses).
 New usage of "scmateALT" is discouraged (0 uses).
-New usage of "sdom1OLD" is discouraged (0 uses).
 New usage of "selsALT" is discouraged (1 uses).
 New usage of "sepexlem" is discouraged (1 uses).
 New usage of "seq1hcau" is discouraged (0 uses).
@@ -18984,7 +18958,6 @@ New usage of "sspz" is discouraged (1 uses).
 New usage of "ssralv2" is discouraged (2 uses).
 New usage of "ssralv2VD" is discouraged (0 uses).
 New usage of "ssralvOLD" is discouraged (0 uses).
-New usage of "ssrelOLD" is discouraged (0 uses).
 New usage of "ssrexvOLD" is discouraged (0 uses).
 New usage of "sstr2OLD" is discouraged (0 uses).
 New usage of "sstrALT2" is discouraged (0 uses).
@@ -19219,8 +19192,6 @@ New usage of "w-bnj17" is discouraged (104 uses).
 New usage of "w-bnj19" is discouraged (8 uses).
 New usage of "watfvalN" is discouraged (1 uses).
 New usage of "watvalN" is discouraged (1 uses).
-New usage of "wksonproplemOLD" is discouraged (0 uses).
-New usage of "wksvOLD" is discouraged (0 uses).
 New usage of "wl-embant" is discouraged (0 uses).
 New usage of "wl-impchain-a1-1" is discouraged (1 uses).
 New usage of "wl-impchain-a1-2" is discouraged (1 uses).
@@ -19267,7 +19238,6 @@ New usage of "wl-section-impchain" is discouraged (0 uses).
 New usage of "wl-section-prop" is discouraged (0 uses).
 New usage of "wl-syls1" is discouraged (0 uses).
 New usage of "wl-syls2" is discouraged (0 uses).
-New usage of "wlkResOLD" is discouraged (0 uses).
 New usage of "wvd2" is discouraged (5 uses).
 New usage of "wvd3" is discouraged (3 uses).
 New usage of "wvhc2" is discouraged (5 uses).
@@ -19356,9 +19326,7 @@ Proof modification of "a1ii" is discouraged (1 steps).
 Proof modification of "ab0ALT" is discouraged (33 steps).
 Proof modification of "ab0orvALT" is discouraged (19 steps).
 Proof modification of "abid2fOLD" is discouraged (26 steps).
-Proof modification of "abrexexgOLD" is discouraged (43 steps).
 Proof modification of "abscncfALT" is discouraged (71 steps).
-Proof modification of "abssdvOLD" is discouraged (24 steps).
 Proof modification of "abvALT" is discouraged (36 steps).
 Proof modification of "ackm" is discouraged (71 steps).
 Proof modification of "addltmulALT" is discouraged (497 steps).
@@ -19805,7 +19773,6 @@ Proof modification of "conventions" is discouraged (1 steps).
 Proof modification of "conventions-comments" is discouraged (1 steps).
 Proof modification of "conventions-labels" is discouraged (1 steps).
 Proof modification of "cotrgOLD" is discouraged (99 steps).
-Proof modification of "cotrgOLDOLD" is discouraged (110 steps).
 Proof modification of "csbcnvgALT" is discouraged (112 steps).
 Proof modification of "csbeq2gVD" is discouraged (61 steps).
 Proof modification of "csbfv12gALTVD" is discouraged (322 steps).
@@ -19837,10 +19804,6 @@ Proof modification of "dfdif3OLD" is discouraged (137 steps).
 Proof modification of "dfeu" is discouraged (35 steps).
 Proof modification of "dffr2ALT" is discouraged (64 steps).
 Proof modification of "dffun2OLD" is discouraged (109 steps).
-Proof modification of "dffun2OLDOLD" is discouraged (157 steps).
-Proof modification of "dffun3OLD" is discouraged (72 steps).
-Proof modification of "dffun6OLD" is discouraged (10 steps).
-Proof modification of "dfiun2gOLD" is discouraged (131 steps).
 Proof modification of "dfmo" is discouraged (44 steps).
 Proof modification of "dfsn2ALT" is discouraged (30 steps).
 Proof modification of "dftr5OLD" is discouraged (93 steps).
@@ -19865,7 +19828,6 @@ Proof modification of "dif1enOLD" is discouraged (313 steps).
 Proof modification of "dif1enlemOLD" is discouraged (285 steps).
 Proof modification of "dif1ennnALT" is discouraged (335 steps).
 Proof modification of "difidALT" is discouraged (14 steps).
-Proof modification of "difopabOLD" is discouraged (171 steps).
 Proof modification of "dih2dimbALTN" is discouraged (450 steps).
 Proof modification of "div0OLD" is discouraged (41 steps).
 Proof modification of "div11OLD" is discouraged (119 steps).
@@ -19878,7 +19840,6 @@ Proof modification of "djuexALT" is discouraged (51 steps).
 Proof modification of "dmcosseqOLD" is discouraged (167 steps).
 Proof modification of "dmfexALT" is discouraged (25 steps).
 Proof modification of "dmtrclfvRP" is discouraged (46 steps).
-Proof modification of "dmxpOLD" is discouraged (57 steps).
 Proof modification of "domnlcanOLD" is discouraged (171 steps).
 Proof modification of "domnlcanbOLD" is discouraged (73 steps).
 Proof modification of "dral1ALT" is discouraged (34 steps).
@@ -20091,8 +20052,6 @@ Proof modification of "eliminable3a" is discouraged (7 steps).
 Proof modification of "eliminable3b" is discouraged (8 steps).
 Proof modification of "elintabOLD" is discouraged (75 steps).
 Proof modification of "elnoOLD" is discouraged (66 steps).
-Proof modification of "elopabrOLD" is discouraged (58 steps).
-Proof modification of "elopaelxpOLD" is discouraged (47 steps).
 Proof modification of "elpwgded" is discouraged (23 steps).
 Proof modification of "elpwgdedVD" is discouraged (23 steps).
 Proof modification of "elrefsymrels3" is discouraged (65 steps).
@@ -20350,11 +20309,8 @@ Proof modification of "fsumdvdsmulOLD" is discouraged (538 steps).
 Proof modification of "fuco11bALT" is discouraged (199 steps).
 Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
 Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
-Proof modification of "funimaexgOLD" is discouraged (133 steps).
-Proof modification of "funmoOLD" is discouraged (115 steps).
 Proof modification of "fvilbdRP" is discouraged (27 steps).
 Proof modification of "fvimacnvALT" is discouraged (102 steps).
-Proof modification of "fvmptopabOLD" is discouraged (185 steps).
 Proof modification of "fvn0fvelrnOLD" is discouraged (94 steps).
 Proof modification of "fvprcALT" is discouraged (26 steps).
 Proof modification of "fvssunirnOLD" is discouraged (47 steps).
@@ -20458,7 +20414,6 @@ Proof modification of "iotaexOLD" is discouraged (57 steps).
 Proof modification of "iotassuniOLD" is discouraged (35 steps).
 Proof modification of "iotavalOLD" is discouraged (101 steps).
 Proof modification of "isanmbfmOLD" is discouraged (15 steps).
-Proof modification of "isarep1OLD" is discouraged (106 steps).
 Proof modification of "iscmgmALT" is discouraged (57 steps).
 Proof modification of "iscsgrpALT" is discouraged (57 steps).
 Proof modification of "isdomn2OLD" is discouraged (222 steps).
@@ -20486,7 +20441,6 @@ Proof modification of "iunconnALT" is discouraged (56 steps).
 Proof modification of "iunconnlem2" is discouraged (580 steps).
 Proof modification of "iuneq12dOLD" is discouraged (37 steps).
 Proof modification of "iunidOLD" is discouraged (77 steps).
-Proof modification of "iunopabOLD" is discouraged (117 steps).
 Proof modification of "ivthALT" is discouraged (1080 steps).
 Proof modification of "jaoded" is discouraged (26 steps).
 Proof modification of "jath" is discouraged (318 steps).
@@ -20570,8 +20524,6 @@ Proof modification of "mobidvALT" is discouraged (48 steps).
 Proof modification of "mof0ALT" is discouraged (67 steps).
 Proof modification of "mopickr" is discouraged (77 steps).
 Proof modification of "mptmpoopabbrdOLD" is discouraged (208 steps).
-Proof modification of "mptmpoopabbrdOLDOLD" is discouraged (247 steps).
-Proof modification of "mptmpoopabovdOLD" is discouraged (89 steps).
 Proof modification of "mptssALT" is discouraged (57 steps).
 Proof modification of "mrelatglbALT" is discouraged (66 steps).
 Proof modification of "mrelatlubALT" is discouraged (76 steps).
@@ -20591,7 +20543,6 @@ Proof modification of "nfeu1ALT" is discouraged (25 steps).
 Proof modification of "nfinOLD" is discouraged (27 steps).
 Proof modification of "nfiu1OLD" is discouraged (28 steps).
 Proof modification of "nfopdALT" is discouraged (70 steps).
-Proof modification of "nfralwOLD" is discouraged (27 steps).
 Proof modification of "nfunOLD" is discouraged (37 steps).
 Proof modification of "nfunidALT" is discouraged (33 steps).
 Proof modification of "nfunidALT2" is discouraged (49 steps).
@@ -20658,7 +20609,6 @@ Proof modification of "onfrALTlem5" is discouraged (320 steps).
 Proof modification of "onfrALTlem5VD" is discouraged (320 steps).
 Proof modification of "ontrciOLD" is discouraged (9 steps).
 Proof modification of "onuniorsuciOLD" is discouraged (16 steps).
-Proof modification of "opabresex2d" is discouraged (48 steps).
 Proof modification of "opelopab4" is discouraged (69 steps).
 Proof modification of "opidon2OLD" is discouraged (80 steps).
 Proof modification of "opidonOLD" is discouraged (198 steps).
@@ -20713,7 +20663,6 @@ Proof modification of "pzriprng1ALT" is discouraged (534 steps).
 Proof modification of "pzriprngALT" is discouraged (150 steps).
 Proof modification of "qexALT" is discouraged (64 steps).
 Proof modification of "quoremnn0ALT" is discouraged (360 steps).
-Proof modification of "r19.21vOLD" is discouraged (60 steps).
 Proof modification of "r19.29OLD" is discouraged (39 steps).
 Proof modification of "r19.29rOLD" is discouraged (39 steps).
 Proof modification of "r19.35OLD" is discouraged (72 steps).
@@ -20790,7 +20739,6 @@ Proof modification of "rexeqOLD" is discouraged (11 steps).
 Proof modification of "rexeqbidvvOLD" is discouraged (47 steps).
 Proof modification of "rexeqfOLD" is discouraged (55 steps).
 Proof modification of "reximaOLD" is discouraged (68 steps).
-Proof modification of "rexlimivOLD" is discouraged (23 steps).
 Proof modification of "rexlimivaOLD" is discouraged (13 steps).
 Proof modification of "rexlimivwOLD" is discouraged (14 steps).
 Proof modification of "rexssOLD" is discouraged (44 steps).
@@ -20863,7 +20811,6 @@ Proof modification of "sbsbc" is discouraged (21 steps).
 Proof modification of "sbtALT" is discouraged (12 steps).
 Proof modification of "sbtT" is discouraged (7 steps).
 Proof modification of "scmateALT" is discouraged (236 steps).
-Proof modification of "sdom1OLD" is discouraged (73 steps).
 Proof modification of "selsALT" is discouraged (34 steps).
 Proof modification of "sgrpplusgaopALT" is discouraged (82 steps).
 Proof modification of "sii" is discouraged (145 steps).
@@ -20909,7 +20856,6 @@ Proof modification of "sspwtrALT2" is discouraged (72 steps).
 Proof modification of "ssralv2" is discouraged (83 steps).
 Proof modification of "ssralv2VD" is discouraged (147 steps).
 Proof modification of "ssralvOLD" is discouraged (23 steps).
-Proof modification of "ssrelOLD" is discouraged (198 steps).
 Proof modification of "ssrexvOLD" is discouraged (23 steps).
 Proof modification of "sstr2OLD" is discouraged (49 steps).
 Proof modification of "sstrALT2" is discouraged (81 steps).
@@ -21054,8 +21000,6 @@ Proof modification of "vtoclegftOLD" is discouraged (50 steps).
 Proof modification of "vtoclfOLD" is discouraged (28 steps).
 Proof modification of "vtoclgOLD" is discouraged (25 steps).
 Proof modification of "vtxdusgr0edgnelALT" is discouraged (94 steps).
-Proof modification of "wksonproplemOLD" is discouraged (278 steps).
-Proof modification of "wksvOLD" is discouraged (81 steps).
 Proof modification of "wl-cases2-dnf" is discouraged (85 steps).
 Proof modification of "wl-dfclab" is discouraged (73 steps).
 Proof modification of "wl-embant" is discouraged (12 steps).
@@ -21103,7 +21047,6 @@ Proof modification of "wl-section-impchain" is discouraged (1 steps).
 Proof modification of "wl-section-prop" is discouraged (1 steps).
 Proof modification of "wl-syls1" is discouraged (12 steps).
 Proof modification of "wl-syls2" is discouraged (14 steps).
-Proof modification of "wlkResOLD" is discouraged (50 steps).
 Proof modification of "xpexgALT" is discouraged (84 steps).
 Proof modification of "xpfiOLD" is discouraged (373 steps).
 Proof modification of "xrge0tmdALT" is discouraged (166 steps).
diff --git a/set.mm b/set.mm
index 178dc87fcd..766e010ed1 100644
--- a/set.mm
+++ b/set.mm
@@ -29225,15 +29225,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( wi wral pm2.27 ralimdv com12 wn pm2.21 ralrimivw ax-1 ralimi ja impbii
       ) ABEZCDFZABCDFZEARSAQBCDABGHIASRAJQCDABKLBQCDBAMNOP $.
 
-    $( Obsolete version of ~ r19.21v as of 11-Dec-2024.  (Contributed by NM,
-       15-Oct-2003.)  (Proof shortened by Andrew Salmon, 30-May-2011.)  Reduce
-       dependencies on axioms.  (Revised by Wolf Lammen, 2-Jan-2020.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    r19.21vOLD $p |- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) ) $=
-      ( cv wcel wi wal wral bi2.04 albii 19.21v bitri df-ral imbi2i 3bitr4i ) C
-      EDFZABGZGZCHZAQBGZCHZGZRCDIABCDIZGTAUAGZCHUCSUECQABJKAUACLMRCDNUDUBABCDNO
-      P $.
-
     $( Restricted quantifier version of one direction of ~ 19.37v .  (The other
        direction holds iff ` A ` is nonempty, see ~ r19.37zv .)  (Contributed
        by NM, 2-Apr-2004.)  Reduce axiom usage.  (Revised by Wolf Lammen,
@@ -29261,17 +29252,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       DHNBMBBCDBIJKL $.
   $}
 
-  ${
-    $d x ps $.
-    rexlimivOLD.1 $e |- ( x e. A -> ( ph -> ps ) ) $.
-    $( Obsolete version of ~ rexlimiv as of 19-Dec-2024.)  (Contributed by NM,
-       20-Nov-1994.)  Reduce dependencies on axioms.  (Revised by Wolf Lammen,
-       14-Jan-2020.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    rexlimivOLD $p |- ( E. x e. A ph -> ps ) $=
-      ( wi wral wrex rgen r19.23v mpbi ) ABFZCDGACDHBFLCDEIABCDJK $.
-  $}
-
   ${
     $d x ps $.
     rexlimivaOLD.1 $e |- ( ( x e. A /\ ph ) -> ps ) $.
@@ -30581,13 +30561,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( wral cv wcel nfcri nf5ri hbral nf5i ) ACDGBABCDCHDIBBCDEJKABFKLM $.
     $( $j usage 'nfralw' avoids 'ax-13'; $)
 
-    $( Obsolete version of ~ nfralw as of 13-Dec-2024.  (Contributed by NM,
-       1-Sep-1999.)  (Revised by GG, 10-Jan-2024.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    nfralwOLD $p |- F/ x A. y e. A ph $=
-      ( wral wnf wtru nftru wnfc a1i nfraldw mptru ) ACDGBHIABCDCJBDKIELABHIFLM
-      N $.
-
     $( 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
@@ -38787,13 +38760,6 @@ many things are technically classes despite morally (and provably) being
     abssdv $p |- ( ph -> { x | ps } C_ A ) $=
       ( cab cv wcel ss2abdv abid1 sseqtrrdi ) ABCFCGDHZCFDABLCEICDJK $.
     $( $j usage 'abssdv' avoids 'ax-10' 'ax-11' 'ax-12'; $)
-
-    $( Obsolete version of ~ abssdv as of 12-Dec-2024.  (Contributed by NM,
-       20-Jan-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    abssdvOLD $p |- ( ph -> { x | ps } C_ A ) $=
-      ( cv wcel wi wal cab wss alrimiv abss sylibr ) ABCFDGHZCIBCJDKAOCELBCDMN
-      $.
   $}
 
   ${
@@ -47305,18 +47271,6 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
 
   ${
     $d y z w A $.  $d y z w B $.  $d w C z $.  $d w x y z $.
-    $( Obsolete version of ~ dfiun2g as of 11-Dec-2024.  (Contributed by NM,
-       23-Mar-2006.)  (Proof shortened by Andrew Salmon, 25-Jul-2011.)  (Proof
-       shortened by Rohan Ridenour, 11-Aug-2023.)  (New usage is discouraged.)
-       (Proof modification is discouraged.) $)
-    dfiun2gOLD $p |- ( A. x e. A B e. C ->
-                  U_ x e. A B = U. { y | E. x e. A y = B } ) $=
-      ( vz wcel wral ciun cv wceq wrex cab cuni wa wex nfra1 wb rspa bitrdi syl
-      clel3g rexbida rexcom4 r19.41v exbii exancom bitri eliun eluniab 3bitr4g
-      eqrdv ) DEGZACHZFACDIZBJZDKZACLZBMNZUNFJZDGZACLZUTUPGZUROBPZUTUOGUTUSGUNV
-      BUQVCOZACLZBPZVDUNVBVEBPZACLVGUNVAVHACUMACQUNAJCGOUMVAVHRUMACSBUTDEUBUAUC
-      VEABCUDTVGURVCOZBPVDVFVIBUQVCACUEUFURVCBUGUHTAUTCDUIURBUTUJUKUL $.
-
     $( Alternate definition of indexed intersection when ` B ` is a set.
        (Contributed by Jeff Hankins, 27-Aug-2009.) $)
     dfiin2g $p |- ( A. x e. A B e. C
@@ -53278,16 +53232,6 @@ necessary if all involved classes exist as sets (i.e. are not proper
       QFABCUJUAUBUCUDVBUTDEJZBOURUTDBERVCUQBVCUSDEJZCOUQUSDCERVDUPCUNADEUESTSTT
       UFDFEUKUGUOBCFUHUI $.
     $( $j usage 'iunopab' avoids 'ax-sep' 'ax-nul' 'ax-pr'; $)
-
-    $( Obsolete version of ~ iunopab as of 11-Dec-2024.  (Contributed by Stefan
-       O'Rear, 20-Feb-2015.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    iunopabOLD $p |- U_ z e. A { <. x , y >. | ph } =
-        { <. x , y >. | E. z e. A ph } $=
-      ( vw cv copab wcel wrex cab cop wceq wex ciun elopab rexcom4 exbii bitri
-      wa rexbii r19.42v abbii df-iun df-opab 3eqtr4i ) FGZABCHZIZDEJZFKUGBGCGLM
-      ZADEJZTZCNZBNZFKDEUHOULBCHUJUOFUJUKATZCNZBNZDEJZUOUIURDEABCUGPUAUSUQDEJZB
-      NUOUQDBEQUTUNBUTUPDEJZCNUNUPDCEQVAUMCUKADEUBRSRSSUCDFEUHUDULBCFUEUF $.
   $}
 
   ${
@@ -53306,17 +53250,6 @@ necessary if all involved classes exist as sets (i.e. are not proper
       CIEPOBCOAJKBCELMN $.
   $}
 
-  ${
-    $d A x y $.  $d R x y $.
-    $( Obsolete version of ~ elopabr as of 11-Dec-2024.  (Contributed by AV,
-       16-Feb-2021.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    elopabrOLD $p |- ( A e. { <. x , y >. | x R y } -> A e. R ) $=
-      ( cv wbr copab wcel cop wceq wa wex elopab df-br eleq1 imbitrrid exlimivv
-      biimpi imp sylbi ) CAEZBEZDFZABGHCUAUBIZJZUCKZBLALCDHZUCABCMUFUGABUEUCUGU
-      CUGUEUDDHZUCUHUAUBDNRCUDDOPSQT $.
-  $}
-
   ${
     $d F f p $.  $d P f p $.  $d W f p $.  $d ch f p $.
     rbropapd.1 $e |- ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } ) $.
@@ -55308,14 +55241,6 @@ of the restricted converse (see ~ cnvrescnv ).  (Contributed by NM,
       ( copab cvv cxp cv wcel wa vex pm3.2i a1i ssopab2i df-xp sseqtrri sseli )
       ABCEZFFGZDRBHFIZCHFIZJZBCESAUBBCUBATUABKCKLMNBCFFOPQ $.
     $( $j usage 'elopaelxp' avoids 'ax-sep' 'ax-nul' 'ax-pr'; $)
-
-    $d A x y $.
-    $( Obsolete version of ~ elopaelxp as of 11-Dec-2024.  (Contributed by
-       Alexander van der Vekens, 23-Jun-2018.)  (New usage is discouraged.)
-       (Proof modification is discouraged.) $)
-    elopaelxpOLD $p |- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) ) $=
-      ( cv cop wceq wa wex copab wcel cvv cxp simpl 2eximi elopab elvv 3imtr4i
-      ) DBECEFGZAHZCIBISCIBIDABCJKDLLMKTSBCSANOABCDPBCDQR $.
   $}
 
   ${
@@ -55510,22 +55435,6 @@ of the restricted converse (see ~ cnvrescnv ).  (Contributed by NM,
       WAVSVNWAVQVLVRVMVPVKCSVPVKDSUOUPUQWAVSABURUSUTVAVDVBECDRVCVEVF $.
     $( $j usage 'ssrel' avoids 'ax-12' 'ax-sep' 'ax-nul' 'ax-pr'; $)
 
-    $( Obsolete version of ~ ssrel as of 11-Dec-2024.  (Contributed by NM,
-       2-Aug-1994.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.)  Remove
-       dependency on ~ ax-sep , ~ ax-nul , ~ ax-pr .  (Revised by KP,
-       25-Oct-2021.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    ssrelOLD $p |- ( Rel A -> ( A C_ B <->
-                A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) ) $=
-      ( vz wrel wss cv cop wcel wi wal ssel alrimivv wceq wex cvv df-ss eleq1
-      wa cxp df-rel sylbb copab cab df-xp df-opab eqtri eqabri simpl sylbi sylg
-      2eximi imim2i imbi12d biimprcd 2alimi 19.23vv sylib com23 a2d alimdv syl5
-      imbitrrdi com12 impbid2 ) CFZCDGZAHZBHZIZCJZVKDJZKZBLALZVHVNABCDVKMNVOVGV
-      HVOVGEHZCJZVPDJZKZELZVHVGVQVPVKOZBPAPZKZELVOVTVGVQVPQQUAZJZKZWCEVGCWDGWFE
-      LCUBECWDRUCWEWBVQWEWAVIQJVJQJTZTZBPAPZWBWIEWDWDWGABUDWIEUEABQQUFWGABEUGUH
-      UIWHWAABWAWGUJUMUKUNULVOWCVSEVOVQWBVRVOWBVQVRVOWAVSKZBLALWBVSKVNWJABWAVSV
-      NWAVQVLVRVMVPVKCSVPVKDSUOUPUQWAVSABURUSUTVAVBVCECDRVDVEVF $.
-
     $( Extensionality principle for relations.  Theorem 3.2(ii) of [Monk1]
        p. 33.  (Contributed by NM, 2-Aug-1994.) $)
     eqrel $p |- ( ( Rel A /\ Rel B ) -> ( A = B <->
@@ -55959,18 +55868,6 @@ of the restricted converse (see ~ cnvrescnv ).  (Contributed by NM,
       FACDEFRBDFOZIZCEOVGCEOZIVFURVGCESVCVHCEBDFSQUQVIBCDEFRUDTUETUOUIUJUFUMCDE
       FRUGUH $.
 
-    $( Obsolete version of ~ difopab as of 19-Dec-2024.  (Contributed by Stefan
-       O'Rear, 17-Jan-2015.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    difopabOLD $p |- ( { <. x , y >. | ph } \ { <. x , y >. | ps } ) =
-        { <. x , y >. | ( ph /\ -. ps ) } $=
-      ( vz vw copab wn wa wrel relopabv cv wcel wsbc sbcan sbcbii opelopabsb wb
-      cvv sbcng cdif reldif ax-mp cop elv notbii 3bitr4ri anbi12i eldif 3bitr4i
-      eqrelriiv ) EFACDGZBCDGZUAZABHZIZCDGZULJUNJACDKULUMUBUCUPCDKELZFLZUDZULMZ
-      UTUMMZHZIZUPDUSNZCURNZUTUNMUTUQMADUSNZUODUSNZIZCURNVGCURNZVHCURNZIVFVDVGV
-      HCUROVEVICURAUODUSOPVAVJVCVKACDURUSQBDUSNZHZCURNZVLCURNZHZVKVCVNVPREVLCUR
-      STUEVHVMCURVHVMRFBDUSSTUEPVBVOBCDURUSQUFUGUHUGUTULUMUIUPCDURUSQUJUK $.
-
     $( Intersection of two Cartesian products.  Exercise 9 of [TakeutiZaring]
        p. 25.  (Contributed by NM, 3-Aug-1994.)  (Proof shortened by Andrew
        Salmon, 27-Aug-2011.)  Avoid ~ ax-10 , ~ ax-12 .  (Revised by SN,
@@ -56924,14 +56821,6 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding).  A more
       ZUJUIUHUKUFMZDKUJULLZDKUNDUHUFCNOUOUPDUHUKABTPUJULDQRUEUMUJUEUMDBSUAUBUCU
       D $.
     $( $j usage 'dmxp' avoids 'ax-10' 'ax-11' 'ax-12'; $)
-
-    $( Obsolete version of ~ dmxp as of 19-Dec-2024.  (Contributed by NM,
-       28-Jul-1995.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    dmxpOLD $p |- ( B =/= (/) -> dom ( A X. B ) = A ) $=
-      ( vy vx c0 wne cxp cdm cv wcel wa copab df-xp dmeqi wex wral n0 ralrimivw
-      wceq biimpi dmopab3 sylib eqtrid ) BEFZABGZHCIAJDIBJZKCDLZHZAUEUGCDABMNUD
-      UFDOZCAPUHASUDUICAUDUIDBQTRUFCDAUAUBUC $.
   $}
 
   $( The domain of a Cartesian square.  (Contributed by NM, 28-Jul-1995.) $)
@@ -58480,19 +58369,6 @@ the restriction (of the relation) to the singleton containing this
       ax-mp imbi1i 19.23v bitr4i alcom ) DEGZFHZAIZCIZUHJZUJUKFJZKZCLZALZUJBIZE
       JUQUKDJMZUMKZCLBLZALUHNUIUPODEPACUHFQUCUOUTAUOUSBLZCLUTUNVACUNURBUAZUMKVA
       ULVBUMBUJUKDEARCRUBUDURUMBUEUFSUSCBUGTST $.
-
-    $( Obsolete version of ~ cotrg as of 19-Dec-2024.  (Contributed by NM,
-       27-Dec-1996.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.)
-       Generalized from its special instance ~ cotr .  (Revised by Richard
-       Penner, 24-Dec-2019.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    cotrgOLDOLD $p |-
-      ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
-      ( ccom wss cv cop wcel wi wal wbr wa wrel wb vex albii bitri relco opelco
-      ssrel ax-mp wex df-br bicomi imbi12i 19.23v bitr4i alcom ) DEGZFHZAIZCIZJ
-      ZULKZUPFKZLZCMZAMZUNBIZENVBUODNOZUNUOFNZLZCMBMZAMULPUMVAQDEUAACULFUCUDUTV
-      FAUTVEBMZCMVFUSVGCUSVCBUEZVDLVGUQVHURVDBUNUODEARCRUBVDURUNUOFUFUGUHVCVDBU
-      IUJSVECBUKTST $.
   $}
 
   ${
@@ -62558,18 +62434,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
       UKCLZDMZKZBCNZOZCPBPAPZKDQUJUSUHUJULUKUIMZUOKZULUNIMZOZCPZAPBPZUSBACDUIIR
       VEVDBPAPUSVDBAUAVCURABCVAUPVBUQUTUMUOULUKDBSASUBUCULUNCSUDUEUFTTUGT $.
     $( $j usage 'dffun2OLD' avoids 'ax-10' 'ax-12'; $)
-
-    $( Obsolete version of ~ dffun2 as of 11-Dec-2024.  (Contributed by NM,
-       29-Dec-1996.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    dffun2OLDOLD $p |- ( Fun A <-> ( Rel A /\
-                 A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) ) $=
-      ( wfun wrel cid wss wa cv wbr wal wex copab 3bitri vex albii alcom bitri
-      wi ccnv weq df-fun df-id sseq2i df-co sseq1i ssopab2bw brcnv anbi1i exbii
-      ccom imbi1i 19.23v bitr4i anbi2i ) DEDFZDDUAZULZGHZIUQAJZBJZDKZVACJDKZIZB
-      CUBZTZCLZBLALZIDUCUTVIUQUTVBVAURKZVDIZAMZVFTZCLZBLZVHALZBLVIUTUSVFBCNZHVL
-      BCNZVQHVOGVQUSBCUDUEUSVRVQBCADURUFUGVLVFBCUHOVNVPBVNVGALZCLVPVMVSCVMVEAMZ
-      VFTVSVLVTVFVKVEAVJVCVDVBVADBPAPUIUJUKUMVEVFAUNUOQVGCARSQVHBAROUPS $.
   $}
 
   ${
@@ -62593,15 +62457,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
       ( wfun wrel cv wbr wmo wal wa weq wi wex dffun6 df-mo albii anbi2i bitri
       ) DEDFZAGBGDHZBIZAJZKTUABCLMBJCNZAJZKABDOUCUETUBUDAUABCPQRS $.
 
-    $( Obsolete version of ~ dffun3 as of 19-Dec-2024.  Alternate definition of
-       function.  (Contributed by NM, 29-Dec-1996.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    dffun3OLD $p |- ( Fun A <-> ( Rel A /\
-                 A. x E. z A. y ( x A y -> y = z ) ) ) $=
-      ( wfun wrel cv wbr wa weq wal wex dffun2 wmo breq2 mo4 df-mo bitr3i albii
-      wi anbi2i bitri ) DEDFZAGZBGZDHZUDCGZDHZIBCJZTCKBKZAKZIUCUFUITBKCLZAKZIAB
-      CDMUKUMUCUJULAUJUFBNULUFUHBCUEUGUDDOPUFBCQRSUAUB $.
-
     $( Alternate definition of a function.  Definition 6.4(4) of
        [TakeutiZaring] p. 24.  (Contributed by NM, 29-Dec-1996.) $)
     dffun4 $p |- ( Fun A <-> ( Rel A /\
@@ -62637,12 +62492,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
 
   ${
     $d x y A $.  $d x y F $.
-    $( Obsolete version of ~ dffun6 as of 19-Dec-2024.  (Contributed by NM,
-       9-Mar-1995.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    dffun6OLD $p |- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) ) $=
-      ( nfcv dffun6f ) ABCACDBCDE $.
-
     $( A function has at most one value for each argument.  (Contributed by NM,
        24-May-1998.)  (Proof shortened by SN, 19-Dec-2024.) $)
     funmo $p |- ( Fun F -> E* y A F y ) $=
@@ -62652,16 +62501,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
       ZASZDLZDACNZOUTUNUOBUMCPQTRUAULUOUSKURULVDUOUSULUTVDVEUBVCUSDBHVABUCVBUNA
       VABUMCUDUEUFUGUOUNAUHUKUNUPAUIUJ $.
     $( $j usage 'funmo' avoids 'ax-12'; $)
-
-    $( Obsolete version of ~ funmo as of 19-Dec-2024.  (Contributed by NM,
-       24-May-1998.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    funmoOLD $p |- ( Fun F -> E* y A F y ) $=
-      ( vx wfun cv wbr cvv wcel wa wi wal wrel dffun6 simplbi brrelex1 ex ancrd
-      wmo syl alrimiv breq1 mobidv imbi2d simprbi 19.21bi vtoclg moanimv sylibr
-      wceq com12 moim sylc ) CEZBAFZCGZBHIZUPJZKZALURASZUPASZUNUSAUNUPUQUNCMZUP
-      UQKUNVBDFZUOCGZASZDLZDACNZOVBUPUQBUOCPQTRUAUNUQVAKUTUQUNVAUNVEKUNVAKDBHVC
-      BUJZVEVAUNVHVDUPAVCBUOCUBUCUDUNVEDUNVBVFVGUEUFUGUKUQUPAUHUIUPURAULUM $.
   $}
 
   $( A function is a relation.  (Contributed by NM, 1-Aug-1994.) $)
@@ -63397,20 +63236,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
     $( $j usage 'funimaexg' avoids 'ax-10' 'ax-12'; $)
   $}
 
-  ${
-    $d w B $.  $d x y z w A $.
-    $( Obsolete version of ~ funimaexg as of 19-Dec-2024.  (Contributed by NM,
-       10-Sep-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    funimaexgOLD $p |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) $=
-      ( vw vx vy vz wcel wfun cima cvv cv wceq imaeq2 eleq1d wal wex wel bitri
-      wi imbi2d cop dffun5 wa wb nfv axrep4 isset cab dfima3 eqeq2i eqabb exbii
-      wrel sylibr simplbiim vtoclg impcom ) BCHAIZABJZKHZUSADLZJZKHZTUSVATDBCVB
-      BMZVDVAUSVEVCUTKVBBANOUAUSAUNELFLZUBAHZVFGLZMTFPGQEPZVDEFGAUCVIFGREDRVGUD
-      EQZUEFPZGQZVDVGEFGDVGGUFUGVDVHVCMZGQVLGVCUHVMVKGVMVHVJFUIZMVKVCVNVHEFAVBU
-      JUKVJFVHULSUMSUOUPUQUR $.
-  $}
-
   ${
     zfrep5.1 $e |- B e. _V $.
     $( The image of a set under any function is also a set.  Equivalent of
@@ -63436,16 +63261,6 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
       vex cop nfs1v nfv sbequ12r cbvrexw 3bitri ) EGZABCHZDIJFGZUFUGKZFDLACEMZB
       FMZFDLUJBDLFUFUGDESNUIUKFDUIUHUFTUGJUKUHUFUGOABCFEPQRUKUJFBDUJBFUAUJFUBUJ
       FBUCUDUE $.
-
-    $( Obsolete version of ~ isarep1 as of 19-Dec-2024.  (Contributed by NM,
-       26-Oct-2006.)  (Proof shortened by Mario Carneiro, 4-Dec-2016.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    isarep1OLD $p |- ( b e. ( { <. x , y >. | ph } " A ) <->
-                 E. x e. A [ b / y ] ph ) $=
-      ( vz copab cima wcel wbr wrex wsb vex elima cop wsbc df-br sbsbc 3bitri
-      cv opelopabsb sbbii bitr2i rexbii nfs1v nfv sbequ12r cbvrexw ) ETZABCGZDH
-      IFTZUIUJJZFDKACELZBFLZFDKUMBDKFUIUJDEMNULUNFDULUKUIOUJIACUIPZBUKPZUNUKUIU
-      JQABCUKUIUAUNUOBFLUPUMUOBFACERUBUOBFRUCSUDUNUMFBDUMBFUEUMFUFUMFBUGUHS $.
   $}
 
   ${
@@ -72489,19 +72304,6 @@ ordered pairs (for use in defining operations).  This is a special case
       FQPABCFGPMNO $.
   $}
 
-  ${
-    $d ph x $.  $d ph y $.
-    opabresex2d.1 $e |- ( ( ph /\ x ( W ` G ) y ) -> ps ) $.
-    opabresex2d.2 $e |- ( ph -> { <. x , y >. | ps } e. V ) $.
-    $( Obsolete version of ~ opabresex2 as of 13-Dec-2024.  (Contributed by
-       Alexander van der Vekens, 1-Nov-2017.)  (Revised by AV, 15-Jan-2021.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    opabresex2d $p |- ( ph -> { <. x , y >. |
-                                ( x ( W ` G ) y /\ th ) } e. _V ) $=
-      ( cv cfv wbr wi wal copab wcel wa cvv ex alrimivv opabbrex syl2anc ) ADKE
-      KFHLZMZBNZEODOBDEPGQUECRDEPSQAUFDEAUEBITUAJBCDEUDGUBUC $.
-  $}
-
   ${
     $d F x y z $.  $d Z x y z $.  $d ps z $.
     fvmptopab.1 $e |- ( z = Z -> ( ph <-> ps ) ) $.
@@ -72522,26 +72324,6 @@ ordered pairs (for use in defining operations).  This is a special case
       TUIUJHFTUKVCULUMUNUO $.
   $}
 
-  ${
-    $d F z $.  $d Z x y z $.  $d ph x y z $.  $d ps z $.
-    fvmptopabOLD.1 $e |- ( ( ph /\ z = Z ) -> ( ch <-> ps ) ) $.
-    fvmptopabOLD.2 $e |- ( ph -> { <. x , y >. | x ( F ` Z ) y } e. _V ) $.
-    fvmptopabOLD.3 $e |- M = ( z e. _V |-> { <. x , y >. |
-                                             ( x ( F ` z ) y /\ ch ) } ) $.
-    $( Obsolete version of ~ fvmptopab as of 13-Dec-2024.  (Contributed by AV,
-       31-Jan-2021.)  (Revised by AV, 29-Oct-2021.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    fvmptopabOLD $p |- ( ph -> ( M ` Z )
-                             = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) $=
-      ( cvv wcel cfv cv wbr wa wal c0 copab wceq wi fveq2 breqd adantll anbi12d
-      wb adantl opabbidv simpl id gen2 opabbrex sylancr fvmptd2 ex wn fvprc br0
-      mtbiri intnanrd alrimivv opab0 sylibr eqtr4d a1d pm2.61i ) IMNZAIHOZDPZEP
-      ZIGOZQZBRZDEUAZUBZUCVIAVQVIARZFIVKVLFPZGOZQZCRZDEUAVPMHMLVRVSIUBZRZWBVODE
-      WDWAVNCBWCWAVNUHVRWCVTVMVKVLVSIGUDUEUIAWCCBUHVIJUFUGUJVIAUKVRVNVNUCZESDSV
-      NDEUAMNZVPMNWEDEVNULUMAWFVIKUIVNBDEVMMUNUOUPUQVIURZVQAWGVJTVPIHUSWGVOURZE
-      SDSVPTUBWGWHDEWGVNBWGVNVKVLTQVKVLUTWGVMTVKVLIGUSUEVAVBVCVODEVDVEVFVGVH $.
-  $}
-
   ${
     $d A r s t u v w $.  $d B r s t u v w $.  $d F r s t u v w $.
     $( Condition for an operation to be one-to-one.  (Contributed by Jeff
@@ -78562,25 +78344,6 @@ as a separate axiom in an axiom system (such as Kunen's) that uses this
       ( wcel cv wceq wmo wal wrex cab cvv moeq ax-gen axrep6g mpan2 ) CEFBGDHZB
       IZAJRACKBLMFSABDNORABCEPQ $.
     $( $j usage 'abrexexg' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-pr' 'ax-un'; $)
-
-    $( Obsolete version of ~ abrexexg as of 11-Dec-2024.  EDITORIAL:  Comment
-       kept since the line of equivalences to ~ ax-rep is different.
-
-       Existence of a class abstraction of existentially restricted sets.  The
-       class ` B ` can be thought of as an expression in ` x ` (which is
-       typically a free variable in the class expression substituted for
-       ` B ` ) and the class abstraction appearing in the statement as the
-       class of values ` B ` as ` x ` varies through ` A ` .  If the "domain"
-       ` A ` is a set, then the abstraction is also a set.  Therefore, this
-       statement is a kind of Replacement.  This can be seen by tracing back
-       through the path ~ mptexg , ~ funex , ~ fnex , ~ resfunexg , and
-       ~ funimaexg .  See also ~ abrexex2g .  There are partial converses under
-       additional conditions, see for instance ~ abnexg .  (Contributed by NM,
-       3-Nov-2003.)  (Proof shortened by Mario Carneiro, 31-Aug-2015.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    abrexexgOLD $p |- ( A e. V -> { y | E. x e. A y = B } e. _V ) $=
-      ( wcel wceq wrex cab cmpt crn cvv eqid rnmpt mptexg rnexg syl eqeltrrid
-      cv ) CEFZBSDGACHBIACDJZKZLABCDUAUAMNTUALFUBLFACDEOUALPQR $.
   $}
 
   ${
@@ -80050,53 +79813,6 @@ Power Set ( ~ ax-pow ).  (Contributed by Mario Carneiro, 20-May-2013.)
       DUEUTUSUKULUMLUNMURUFUGUOIUDZUQUTUKULVAUPURUMUNUOIDUHUIUGSUJ $.
   $}
 
-  ${
-    $d A a b g $.  $d B a b g $.  $d D a b g $.  $d G a b f g h $.  $d W g $.
-    $d X a b f g h $.  $d Y a b f g h $.  $d ph f h $.
-    mptmpoopabbrdOLD.g $e |- ( ph -> G e. W ) $.
-    mptmpoopabbrdOLD.x $e |- ( ph -> X e. ( A ` G ) ) $.
-    mptmpoopabbrdOLD.y $e |- ( ph -> Y e. ( B ` G ) ) $.
-    mptmpoopabbrdOLD.v $e |- ( ph -> { <. f , h >. | ps } e. V ) $.
-    mptmpoopabbrdOLD.r $e |- ( ( ph /\ f ( D ` G ) h ) -> ps ) $.
-    ${
-      $d ta g $.  $d th a b $.
-      mptmpoopabbrdOLD.1 $e |- ( ( a = X /\ b = Y ) -> ( ta <-> th ) ) $.
-      mptmpoopabbrdOLD.2 $e |- ( g = G -> ( ch <-> ta ) ) $.
-      mptmpoopabbrdOLD.m $e |- M = ( g e. _V
-                                    |-> ( a e. ( A ` g ) , b e. ( B ` g )
-                           |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) ) $.
-      $( Obsolete version of ~ mptmpoopabbrd as of 13-Dec-2024.  (Contributed
-         by Alexander van Vekens, 8-Nov-2017.)  (Revised by AV, 15-Jan-2021.)
-         (Proof modification is discouraged.)  (New usage is discouraged.) $)
-      mptmpoopabbrdOLDOLD $p |- ( ph -> ( X ( M ` G ) Y )
-                               = { <. f , h >. | ( th /\ f ( D ` G ) h ) } ) $=
-        ( cfv co cv wbr copab cmpo wcel wceq cvv fveq2 breqd anbi12d mpoeq123dv
-        wa opabbidv elex adantr fvex pm3.2i mpoexga fvmptd3 syl2anc oveqd ancom
-        mp1i opabbii opabresex2d eqeltrid anbi1d eqid ovmpoga syl3anc eqtrd ) A
-        PQLMUHZUIPQRSLFUHZLGUHZEIUJZKUJZLHUHZUKZVAZIKULZUMZUIZDWGVAZIKULZAWAWJP
-        QALOUNZWNWAWJUOTTWNWNVAZJLRSJUJZFUHZWPGUHZCWDWEWPHUHZUKZVAZIKULZUMWJUPM
-        UPUGWPLUOZRSWQWRXBWBWCWIWPLFUQWPLGUQXCXAWHIKXCCEWTWGUFXCWSWFWDWEWPLHUQU
-        RUSVBUTWNLUPUNWNLOVCVDWBUPUNZWCUPUNZVAWJUPUNWOXDXELFVELGVEVFRSWBWCWIUPU
-        PVGVLVHVIVJAPWBUNQWCUNWMUPUNWKWMUOUAUBAWMWGDVAZIKULUPWLXFIKDWGVKVMABDIK
-        LNHUDUCVNVORSPQWBWCWIWMWJUPRUJPUOSUJQUOVAZWHWLIKXGEDWGUEVPVBWJVQVRVSVT
-        $.
-    $}
-
-    $d C a b g $.
-    mptmpoopabovdOLD.m $e |- M = ( g e. _V |->
-      ( a e. ( A ` g ) , b e. ( B ` g )
-        |-> { <. f , h >. | ( f ( a ( C ` g ) b ) h /\ f ( D ` g ) h ) } ) ) $.
-    $( Obsolete version of ~ mptmpoopabovd as of 13-Dec-2024.  (Contributed by
-       Alexander van der Vekens, 8-Nov-2017.)  (Revised by AV, 15-Jan-2021.)
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    mptmpoopabovdOLD $p |- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. |
-                              ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } ) $=
-      ( cv cfv co wbr wceq wa oveq12 breqd fveq2 oveqd mptmpoopabbrdOLDOLD ) AB
-      GUDZIUDZPUDZQUDZHUDZEUEZUFZUGUOUPNOJEUEZUFZUGUOUPUQURVBUFZUGCDFGHIJKLMNOP
-      QRSTUAUBUQNUHUROUHUIVDVCUOUPUQNUROVBUJUKUSJUHZVAVDUOUPVEUTVBUQURUSJEULUMU
-      KUCUN $.
-  $}
-
   ${
     $d A a b s t x y $.  $d B a b s t x y $.  $d C a b s t $.  $d D a b s t $.
     $d E a b $.  $d U a b x y $.  $d V a b x y $.  $d X a b s t x y $.
@@ -96448,15 +96164,6 @@ singletons being the empty set ( ` A e/ _V ` ).  (Contributed by AV,
     $( $j usage 'sdom1' avoids 'ax-pow' 'ax-un'; $)
   $}
 
-  $( Obsolete version of ~ sdom1 as of 12-Dec-2024.  (Contributed by Stefan
-     O'Rear, 28-Oct-2014.)  (Proof modification is discouraged.)
-     (New usage is discouraged.) $)
-  sdom1OLD $p |- ( A ~< 1o <-> A = (/) ) $=
-    ( c1o csdm wbr c0 wceq wn cdom domnsym con2i 0sdom1dom sylnibr wcel relsdom
-    cvv wb brrelex1i 0sdomg necon2bbid syl mpbird 1oex 0sdom mpbir breq1 mpbiri
-    wne 1n0 impbii ) ABCDZAEFZUJUKEACDZGZUJBAHDZULUNUJBAIJAKLUJAOMZUKUMPABCNQUO
-    ULAEAORSTUAUKUJEBCDZUPBEUGUHBUBUCUDAEBCUEUFUI $.
-
   $( Two ways to express "at most one".  (Contributed by Stefan O'Rear,
      28-Oct-2014.) $)
   modom $p |- ( E* x ph <-> { x | ph } ~<_ 1o ) $=
@@ -449839,15 +449546,6 @@ in common (for j=1, ... , k).  In contrast to the definition in Aksoy et
        shortened by SN, 11-Dec-2024.) $)
     wksv $p |- { <. f , p >. | f ( Walks ` G ) p } e. _V $=
       ( cv cwlks cfv wbr copab fvex opabss ssexi ) ADCDBEFZGACHLBEIACLJK $.
-
-    $( Obsolete version of ~ wksv as of 11-Dec-2024.  (Contributed by AV,
-       15-Jan-2021.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    wksvOLD $p |- { <. f , p >. | f ( Walks ` G ) p } e. _V $=
-      ( cvtx cfv cvv wcel cwlks wbr copab fvex ciedg cdm cword dmex wrdexg mp1i
-      cv eqid adantl wlkf wlkpwrd opabex2 ax-mp ) BDEZFGZARZCRZBHEIZACJFGBDKUFU
-      IACBLEZMZNZUENZFFUKFGULFGUFUJBLKOUKFPQUEFPUIUGULGUFUHUGBUJUJSUATUIUHUMGUF
-      UHUGBUEUESUBTUCUD $.
   $}
 
   $( The sequence of vertices of a walk cannot be empty, i.e. a walk always
@@ -450315,18 +450013,6 @@ in common (for j=1, ... , k).  In contrast to the definition in Aksoy et
       UCABUSCDUSULZUDUEUOUTVCBVAUMUTVCUFUNUMUTVCUSDUQURVDUGUHUIUJUK $.
   $}
 
-  ${
-    $d G f p $.
-    wlkResOLD.1 $e |- ( f ( W ` G ) p -> f ( Walks ` G ) p ) $.
-    $( Obsolete version of ~ opabresex2 as of 13-Dec-2024.  (Contributed by
-       Alexander van der Vekens, 1-Nov-2017.)  (Revised by AV, 30-Dec-2020.)
-       (Proof shortened by AV, 15-Jan-2021.)  (New usage is discouraged.)
-       (Proof modification is discouraged.) $)
-    wlkResOLD $p |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V $=
-      ( cv cfv wbr cwlks wi wal copab cvv wcel wa gen2 wksv opabbrex mp2an ) BG
-      ZEGZCDHZIZUAUBCJHIZKZELBLUEBEMNOUDAPBEMNOUFBEFQBCERUEABEUCNST $.
-  $}
-
   $( If there is a walk in the null graph (a class without vertices), it would
      be the pair consisting of empty sets.  (Contributed by Alexander van der
      Vekens, 2-Sep-2018.)  (Revised by AV, 5-Mar-2021.) $)
@@ -451203,37 +450889,6 @@ segment of the trail (of length ` N ` ) forms a trail on the subgraph
       WBTZVOTWCVNXCVOVKVLVMVAVBVKWBVOVDVEVFVPVJVTVPVJVTPVGVHVIVNVOVTVDVF $.
   $}
 
-  ${
-    $d A a b f g p $.  $d B a b f g p $.  $d G a b f g p $.  $d O a b g $.
-    $d Q a b g $.  $d V a b f g p $.
-    wksonproplemOLD.v $e |- V = ( Vtx ` G ) $.
-    wksonproplemOLD.b $e |- ( ( ( G e. _V /\ A e. V /\ B e. V )
-                     /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( W ` G ) B ) P
-                          <-> ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) $.
-    wksonproplemOLD.d $e |- W = ( g e. _V
-                        |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g )
-                              |-> { <. f , p >. | ( f ( a ( O ` g ) b ) p
-                                                    /\ f ( Q ` g ) p ) } ) ) $.
-    wksonproplemOLD.w $e |- ( ( ( G e. _V /\ A e. V /\ B e. V )
-                               /\ f ( Q ` G ) p ) -> f ( Walks ` G ) p ) $.
-    $( Obsolete version of ~ wksonproplem as of 13-Dec-2024.  (Contributed by
-       AV, 16-Jan-2021.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    wksonproplemOLD $p |- ( F ( A ( W ` G ) B ) P
-                 -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V )
-                      /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) ) $=
-      ( cvv wa cfv co wbr wcel w3a wi fvexi cv cwlks simp1 simp2 eleqtrdi simp3
-      cvtx copab wksv mptmpoopabovdOLD wceq fveq2 eqtr4di oveqd breqd bropfvvvv
-      anbi12d mp2an 3anass anbi1i df-3an bitr4i sylibr biimpd imdistani mpancom
-      a1i ) GCABHKUAUBUCZHSUDZAJUDZBJUDZUEZGSUDCSUDTZTZGCABHIUAZUBZUCGCHDUAZUCT
-      ZTZVSVTWEUEWAVOWFVOVPVQVRTZVTUEZWAJSUDZWIVOWHUFJHUNOUGZWJEUHZLUHZMUHZNUHZ
-      FUHZIUAZUBZUCZWKWLWODUAZUCZTWKWLWMWNWBUBZUCZWKWLWDUCZTWKWLWCUCXCTHABGJJSL
-      CKWOUNUAZXDSSFMNEQVSWKWLHUIUAUCZUNUNIDEFLHKSSABMNVPVQVRUJVSAJHUNUAZVPVQVR
-      UKOULVSBJXFVPVQVRUMOULXEELUOSUDVSEHLUPVNRQUQWOHURZXDXFJWOHUNUSOUTZXHXGWRX
-      BWTXCXGWQXAWKWLXGWPWBWMWNWOHIUSVAVBXGWSWDWKWLWOHDUSVBVDVCVEWAVPWGTZVTTWHV
-      SXIVTVPVQVRVFVGVPWGVTVHVIVJWAVOWEWAVOWEPVKVLVMVSVTWEVHVJ $.
-  $}
-
   ${
     $d A a b f g p $.  $d B a b f g p $.  $d G a b f g p $.  $d V a b f g p $.
     trlsonfval.v $e |- V = ( Vtx ` G ) $.