From 77457b88e25ae36fece5b0db8aa46b0cb07d21a5 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Fri, 19 Dec 2025 22:33:50 +0100
Subject: [PATCH 1/2] delete outdated OLD

---
 discouraged |  57 -------
 set.mm      | 417 ----------------------------------------------------
 2 files changed, 474 deletions(-)

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..7bd04ae097 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 ) $.
@@ -807570,78 +807225,6 @@ to anything to right of it (so-called "global monotonicity").  Deduction
       VAVBUKVCVFWDVGVHWEVIVJWFVGTFEVQWEADHVPVKVLTEFVQWGRVMTEFBVRCVLT $.
   $}
 
-  $( Complex conjugation operator is not a polynomial with complex
-     coefficients.  Indeed; if it was, then multiplying ` x ` conjugate by
-     ` x ` itself and adding 1 would yield a nowhere-zero non-constant
-     polynomial, contrary to the ~ fta .  (Contributed by Ender Ting,
-     8-Dec-2025.) $)
-  cjnpoly $p |- -. * e. ( Poly ` CC ) $=
-    ( vx ccj cc cfv wcel c1 cidp cmul caddc cc0 wceq cvv wfn cid a1i ax-mp cdgr
-    co cn ax-1cn cply cv csn cxp cof wrex cnex 1ex fconstmpt fnmpti wtru fnresi
-    wa cres df-idp fneq1i mpbir wf cjf ffn inidm offn mptru fnfvof mpanl12 mpan
-    fvconst2 oveq1d eqtrd fveq1i fvres eqtrid fvi oveq2d 1red cjmulrcl clt 0lt1
-    wbr cjmulge0 addgtge0d gt0ne0d eqnetrd neneqd nrex wss plyconst mp2an plyid
-    ssid plymulcl plyaddcl sylancr cn0 dgrcl nn0p1nn nn0cn addcomd eleq1d mpbid
-    1cnd syl c0p wne cr 1re cjre ax-1ne0 eqnetri ne0p eqtri pm3.2i dgrid eqcomi
-    eqid dgrmul mpan2 mpbird nngt0d dgradd2 syl3anc biimprd mpd fta syl2anc mto
-    0dgr ) BCUADZEZAUBZCFUCUDZGBHUERZIUERZDZJKZACUFZYOACYJCEZYNJYQYNFYJYJBDZHRZ
-    IRZJYQYNFYJYLDZIRZYTYQYNYJYKDZUUAIRZUUBCLEZYQYNUUDKZUGYKCMYLCMZUUEYQUMZUUFA
-    CFYKUHACFUIUJUUGUKCCHCGBLLGCMZUKUUINCUNZCMCULCGUUJUOUPUQZOBCMZUKCCBURUULUSC
-    CBUTPZOUUEUKUGOZUUNCVAVBVCCIYKYLLYJVDVEVFYQUUCFUUAICFYJUHVGVHVIYQUUAYSFIYQU
-    UAYJGDZYRHRZYSUUEYQUUAUUPKZUGUUIUULUUHUUQUUKUUMCHGBLYJVDVEVFYQUUOYJYRHYQUUO
-    YJNDZYJYQUUOYJUUJDUURYJGUUJUOVJYJCNVKVLYJCVMVIVHVIVNVIYQYTYQFYSYQVOYJVPJFVQ
-    VSYQVROYJVTWAWBWCWDWEYIYMYHEZYMQDZSEZYPYIYKYHEZYLYHEZUUSCCWFZFCEZUVBCWJZTFC
-    WGWHZGYHEZYIUVCUVDUVEUVHUVFTCWIWHZCGBWKVFZCYKYLWLWMYIYLQDZSEZUVAYIUVLFBQDZI
-    RZSEZYIUVMWNEZUVOCBWOUVPUVMFIRZSEUVOUVMWPUVPUVQUVNSUVPUVMFUVMWQUVPXAWRWSWTX
-    BYIUVKUVNSYIBXCXDZUVKUVNKZUVEFBDZJXDUVRTUVTFJFXEEUVTFKXFFXGPXHXIFBXJWHUVHGX
-    CXDZUMYIUVRUMUVSUVHUWAUVIUVEFGDZJXDUWATUWBFJUWBFNDZFUWBFUUJDZUWCFGUUJUOVJUV
-    EUWDUWCKTFCNVKPXKFLEUWCFKUHFLVMPXKXHXIFGXJWHXLCGBFUVMGQDFXMXNUVMXOXPVFXQWSX
-    RZYIUVAUVLYIUUTUVKSYIUVBUVCJUVKVQVSUUTUVKKUVBYIUVGOUVJYIUVKUWEXSCYKYLJUVKYK
-    QDZJUVEUWFJKTFYGPXNUVKXOXTYAWSYBYCACYMYDYEYF $.
-
-  $( The tangent function is not a polynomial with complex coefficients, as it
-     is not defined on the whole complex plane.  (Contributed by Ender Ting,
-     10-Dec-2025.) $)
-  tannpoly $p |- -. tan e. ( Poly ` CC ) $=
-    ( vx ctan cc cply cfv wcel cpi cdiv co cdm ccos cc0 wceq biimprd ax-mp cosf
-    mpi wf fdm mto ccnv csn cdif cima coshalfpi c0ex snid eleq1 eldifn mt2 picn
-    c2 wb halfcl eleq2i mpbir wfun ffun fvimacnv mpan mtbi cv csin df-tan sseli
-    dmmptss plyf eleq2 3syl ) BCDEFZGULHIZBJZFZVMVKKUACLUBZUCZUDZFZVKKEZVOFZVQV
-    SVRVNFZVRLMZVTUEWALVNFZVTLUFUGWAVTWBVRLVNUHNQOVRCVNUIUJVKKJZFZVSVQUMZWDVKCF
-    ZGCFWFUKGUNOZWCCVKCCKRZWCCMPCCKSOUOUPKUQZWDWEWHWIPCCKUROVKVOKUSUTOVAVLVPVKA
-    VPAVBZVCEWJKEHIBAVDVFVETVJCCBRVLCMZVMCBVGCCBSWKWFVMWGWKVMWFVLCVKVHNQVIT $.
-
-  ${
-    $d x y z t $.
-    $( Sine function is not a polynomial with complex coefficients.  Indeed, it
-       has infinitely many zeros but is not constant zero, contrary to ~ fta1 .
-       (Contributed by Ender Ting, 10-Dec-2025.) $)
-    sinnpoly $p |- -. sin e. ( Poly ` CC ) $=
-      ( vz vx vy vt csin cc cfv wcel cc0 c0p wa c4 ax-mp wceq cz cv cpi cmul co
-      syl cply cn cfn nnnfi ccnv csn cima chash cdgr cle wbr wne cr 4re resincl
-      clt sin4lt0 cxp df-0p fveq1i 4cn c0ex fvconst2 eqtri eqcomi breqtri fveq1
-      ltneii necon3i eqid fta1 mpan2 simpld cmpt wf1 wf wmo wal wfn crn wss cvv
-      wral rgen nfcv mptfnf mpbi sinkpi snid eqeltrdi wfun cdm wb sinf ffun a1i
-      ovexd zcn picn mulcl sylancl eleq2i sylibr fvimacnv syl2anc mpbid rnmptss
-      fdmi pm3.2i df-f mpbir cdiv simpr oveq1 simpl pine0 divcan4 mp3an23 eqtrd
-      moeq eqcomd moimi ax-gen vex eleq1w adantr eqeq1 eqeq2d sylan9bbr anbi12d
-      df-mpt braba mobii albii dff12 f1fi nnssz ssfi mto ) EFUAGHZUBUCHZUDYTEUE
-      IUFZUGZUCHZUUAYTUUDUUCUHGEUIGUJUKZYTEJULZUUDUUEKLEGZLJGZULUUFUUGUUHLUMHUU
-      GUMHUNLUOMUUGIUUHUPUQUUHIUUHLFUUBURZGZILJUUIUSUTLFHUUJINVAFILVBVCMVDVEVFV
-      HEJUUGUUHLEJVGVIMUUCFEUUCVJVKVLVMUUDOUUCAOAPZQRSZVNZVOZUUAUUNOUUCUUMVPZBP
-      ZCPZUUMUKZBVQZCVRZKUUOUUTUUOUUMOVSZUUMVTUUCWAZKUVAUVBUULWBHZAOWCUVAUVCAOU
-      UKOHZUUKQRWQWDAOUULAOWEWFWGUULUUCHZAOWCUVBUVEAOUVDUULEGZUUBHZUVEUVDUVFIUU
-      BUUKWHIVBWIWJUVDEWKZUULEWLZHZUVGUVEWMUVHUVDFFEVPUVHWNFFEWOMWPUVDUULFHZUVJ
-      UVDUUKFHQFHZUVKUUKWRWSUUKQWTXAUVIFUULFFEWNXHXBXCUULUUBEXDXEXFWDAOUULUUCUU
-      MUUMVJXGMXIOUUCUUMXJXKUUTUUPOHZUUQUUPQRSZNZKZBVQZCVRUVQCUUPUUQQXLSZNZBVQU
-      VQBUVRXTUVPUVSBUVPUVRUUPUVPUVRUVNQXLSZUUPUVPUVOUVRUVTNUVMUVOXMUUQUVNQXLXN
-      TUVPUUPFHZUVTUUPNZUVPUVMUWAUVMUVOXOUUPWRTUWAUVLQIULUWBWSXPUUPQXQXRTXSYAYB
-      MYCUUSUVQCUURUVPBUVDDPZUULNZKUVPADUUPUUQUUMBYDCYDUUKUUPNZUWCUUQNZKUVDUVMU
-      WDUVOUWEUVDUVMWMUWFABOYEYFUWFUWDUUQUULNUWEUVOUWCUUQUULYGUWEUULUVNUUQUUKUU
-      PQRXNYHYIYJADOUULYKYLYMYNXKXIBCOUUCUUMYOXKUUDUUNKOUCHZUUAOUUCUUMYPUWGUBOW
-      AUUAYQOUBYRVLTVLTYS $.
-  $}
-
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Scratchpad for probability theory

From 2e8d640aac52e65b47378c3bee477b24ecded848 Mon Sep 17 00:00:00 2001
From: Wolf Lammen <wolf.lammen@gmail.com>
Date: Sat, 20 Dec 2025 18:23:52 +0100
Subject: [PATCH 2/2] restore accidentially deleted theorems

---
 set.mm | 72 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)

diff --git a/set.mm b/set.mm
index 7bd04ae097..766e010ed1 100644
--- a/set.mm
+++ b/set.mm
@@ -807225,6 +807225,78 @@ to anything to right of it (so-called "global monotonicity").  Deduction
       VAVBUKVCVFWDVGVHWEVIVJWFVGTFEVQWEADHVPVKVLTEFVQWGRVMTEFBVRCVLT $.
   $}
 
+  $( Complex conjugation operator is not a polynomial with complex
+     coefficients.  Indeed; if it was, then multiplying ` x ` conjugate by
+     ` x ` itself and adding 1 would yield a nowhere-zero non-constant
+     polynomial, contrary to the ~ fta .  (Contributed by Ender Ting,
+     8-Dec-2025.) $)
+  cjnpoly $p |- -. * e. ( Poly ` CC ) $=
+    ( vx ccj cc cfv wcel c1 cidp cmul caddc cc0 wceq cvv wfn cid a1i ax-mp cdgr
+    co cn ax-1cn cply cv csn cxp cof wrex cnex 1ex fconstmpt fnmpti wtru fnresi
+    wa cres df-idp fneq1i mpbir wf cjf ffn inidm offn mptru fnfvof mpanl12 mpan
+    fvconst2 oveq1d eqtrd fveq1i fvres eqtrid fvi oveq2d 1red cjmulrcl clt 0lt1
+    wbr cjmulge0 addgtge0d gt0ne0d eqnetrd neneqd nrex wss plyconst mp2an plyid
+    ssid plymulcl plyaddcl sylancr cn0 dgrcl nn0p1nn nn0cn addcomd eleq1d mpbid
+    1cnd syl c0p wne cr 1re cjre ax-1ne0 eqnetri ne0p eqtri pm3.2i dgrid eqcomi
+    eqid dgrmul mpan2 mpbird nngt0d dgradd2 syl3anc biimprd mpd fta syl2anc mto
+    0dgr ) BCUADZEZAUBZCFUCUDZGBHUERZIUERZDZJKZACUFZYOACYJCEZYNJYQYNFYJYJBDZHRZ
+    IRZJYQYNFYJYLDZIRZYTYQYNYJYKDZUUAIRZUUBCLEZYQYNUUDKZUGYKCMYLCMZUUEYQUMZUUFA
+    CFYKUHACFUIUJUUGUKCCHCGBLLGCMZUKUUINCUNZCMCULCGUUJUOUPUQZOBCMZUKCCBURUULUSC
+    CBUTPZOUUEUKUGOZUUNCVAVBVCCIYKYLLYJVDVEVFYQUUCFUUAICFYJUHVGVHVIYQUUAYSFIYQU
+    UAYJGDZYRHRZYSUUEYQUUAUUPKZUGUUIUULUUHUUQUUKUUMCHGBLYJVDVEVFYQUUOYJYRHYQUUO
+    YJNDZYJYQUUOYJUUJDUURYJGUUJUOVJYJCNVKVLYJCVMVIVHVIVNVIYQYTYQFYSYQVOYJVPJFVQ
+    VSYQVROYJVTWAWBWCWDWEYIYMYHEZYMQDZSEZYPYIYKYHEZYLYHEZUUSCCWFZFCEZUVBCWJZTFC
+    WGWHZGYHEZYIUVCUVDUVEUVHUVFTCWIWHZCGBWKVFZCYKYLWLWMYIYLQDZSEZUVAYIUVLFBQDZI
+    RZSEZYIUVMWNEZUVOCBWOUVPUVMFIRZSEUVOUVMWPUVPUVQUVNSUVPUVMFUVMWQUVPXAWRWSWTX
+    BYIUVKUVNSYIBXCXDZUVKUVNKZUVEFBDZJXDUVRTUVTFJFXEEUVTFKXFFXGPXHXIFBXJWHUVHGX
+    CXDZUMYIUVRUMUVSUVHUWAUVIUVEFGDZJXDUWATUWBFJUWBFNDZFUWBFUUJDZUWCFGUUJUOVJUV
+    EUWDUWCKTFCNVKPXKFLEUWCFKUHFLVMPXKXHXIFGXJWHXLCGBFUVMGQDFXMXNUVMXOXPVFXQWSX
+    RZYIUVAUVLYIUUTUVKSYIUVBUVCJUVKVQVSUUTUVKKUVBYIUVGOUVJYIUVKUWEXSCYKYLJUVKYK
+    QDZJUVEUWFJKTFYGPXNUVKXOXTYAWSYBYCACYMYDYEYF $.
+
+  $( The tangent function is not a polynomial with complex coefficients, as it
+     is not defined on the whole complex plane.  (Contributed by Ender Ting,
+     10-Dec-2025.) $)
+  tannpoly $p |- -. tan e. ( Poly ` CC ) $=
+    ( vx ctan cc cply cfv wcel cpi cdiv co cdm ccos cc0 wceq biimprd ax-mp cosf
+    mpi wf fdm mto ccnv csn cdif cima coshalfpi c0ex snid eleq1 eldifn mt2 picn
+    c2 wb halfcl eleq2i mpbir wfun ffun fvimacnv mpan mtbi cv csin df-tan sseli
+    dmmptss plyf eleq2 3syl ) BCDEFZGULHIZBJZFZVMVKKUACLUBZUCZUDZFZVKKEZVOFZVQV
+    SVRVNFZVRLMZVTUEWALVNFZVTLUFUGWAVTWBVRLVNUHNQOVRCVNUIUJVKKJZFZVSVQUMZWDVKCF
+    ZGCFWFUKGUNOZWCCVKCCKRZWCCMPCCKSOUOUPKUQZWDWEWHWIPCCKUROVKVOKUSUTOVAVLVPVKA
+    VPAVBZVCEWJKEHIBAVDVFVETVJCCBRVLCMZVMCBVGCCBSWKWFVMWGWKVMWFVLCVKVHNQVIT $.
+
+  ${
+    $d x y z t $.
+    $( Sine function is not a polynomial with complex coefficients.  Indeed, it
+       has infinitely many zeros but is not constant zero, contrary to ~ fta1 .
+       (Contributed by Ender Ting, 10-Dec-2025.) $)
+    sinnpoly $p |- -. sin e. ( Poly ` CC ) $=
+      ( vz vx vy vt csin cc cfv wcel cc0 c0p wa c4 ax-mp wceq cz cv cpi cmul co
+      syl cply cn cfn nnnfi ccnv csn cima chash cdgr cle wbr wne cr 4re resincl
+      clt sin4lt0 cxp df-0p fveq1i 4cn c0ex fvconst2 eqtri eqcomi breqtri fveq1
+      ltneii necon3i eqid fta1 mpan2 simpld cmpt wf1 wf wmo wal wfn crn wss cvv
+      wral rgen nfcv mptfnf mpbi sinkpi snid eqeltrdi wfun cdm wb sinf ffun a1i
+      ovexd zcn picn mulcl sylancl eleq2i sylibr fvimacnv syl2anc mpbid rnmptss
+      fdmi pm3.2i df-f mpbir cdiv simpr oveq1 simpl pine0 divcan4 mp3an23 eqtrd
+      moeq eqcomd moimi ax-gen vex eleq1w adantr eqeq1 eqeq2d sylan9bbr anbi12d
+      df-mpt braba mobii albii dff12 f1fi nnssz ssfi mto ) EFUAGHZUBUCHZUDYTEUE
+      IUFZUGZUCHZUUAYTUUDUUCUHGEUIGUJUKZYTEJULZUUDUUEKLEGZLJGZULUUFUUGUUHLUMHUU
+      GUMHUNLUOMUUGIUUHUPUQUUHIUUHLFUUBURZGZILJUUIUSUTLFHUUJINVAFILVBVCMVDVEVFV
+      HEJUUGUUHLEJVGVIMUUCFEUUCVJVKVLVMUUDOUUCAOAPZQRSZVNZVOZUUAUUNOUUCUUMVPZBP
+      ZCPZUUMUKZBVQZCVRZKUUOUUTUUOUUMOVSZUUMVTUUCWAZKUVAUVBUULWBHZAOWCUVAUVCAOU
+      UKOHZUUKQRWQWDAOUULAOWEWFWGUULUUCHZAOWCUVBUVEAOUVDUULEGZUUBHZUVEUVDUVFIUU
+      BUUKWHIVBWIWJUVDEWKZUULEWLZHZUVGUVEWMUVHUVDFFEVPUVHWNFFEWOMWPUVDUULFHZUVJ
+      UVDUUKFHQFHZUVKUUKWRWSUUKQWTXAUVIFUULFFEWNXHXBXCUULUUBEXDXEXFWDAOUULUUCUU
+      MUUMVJXGMXIOUUCUUMXJXKUUTUUPOHZUUQUUPQRSZNZKZBVQZCVRUVQCUUPUUQQXLSZNZBVQU
+      VQBUVRXTUVPUVSBUVPUVRUUPUVPUVRUVNQXLSZUUPUVPUVOUVRUVTNUVMUVOXMUUQUVNQXLXN
+      TUVPUUPFHZUVTUUPNZUVPUVMUWAUVMUVOXOUUPWRTUWAUVLQIULUWBWSXPUUPQXQXRTXSYAYB
+      MYCUUSUVQCUURUVPBUVDDPZUULNZKUVPADUUPUUQUUMBYDCYDUUKUUPNZUWCUUQNZKUVDUVMU
+      WDUVOUWEUVDUVMWMUWFABOYEYFUWFUWDUUQUULNUWEUVOUWCUUQUULYGUWEUULUVNUUQUUKUU
+      PQRXNYHYIYJADOUULYKYLYMYNXKXIBCOUUCUUMYOXKUUDUUNKOUCHZUUAOUUCUUMYPUWGUBOW
+      AUUAYQOUBYRVLTVLTYS $.
+  $}
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Scratchpad for probability theory