Skip to content

Commit

Permalink
delete outdated OLD theorems (metamath#3742)
Browse files Browse the repository at this point in the history
* delete outdated OLD theorems

* discouraged
  • Loading branch information
wlammen authored Jan 4, 2024
1 parent b8e5ee3 commit 8de506c
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 151 deletions.
26 changes: 0 additions & 26 deletions discouraged
Original file line number Diff line number Diff line change
Expand Up @@ -14062,7 +14062,6 @@ New usage of "cbvalvOLD" is discouraged (0 uses).
New usage of "cbveuALT" is discouraged (0 uses).
New usage of "cbvexsv" is discouraged (2 uses).
New usage of "cbvexvOLD" is discouraged (0 uses).
New usage of "cbvmoOLD" is discouraged (0 uses).
New usage of "cbvrabvOLD" is discouraged (0 uses).
New usage of "cbvrexdva2OLD" is discouraged (0 uses).
New usage of "ccat2s1fvwALT" is discouraged (0 uses).
Expand Down Expand Up @@ -14653,7 +14652,6 @@ New usage of "dfbi1ALT" is discouraged (0 uses).
New usage of "dfch2" is discouraged (0 uses).
New usage of "dfcnqs" is discouraged (4 uses).
New usage of "dfeu" is discouraged (0 uses).
New usage of "dfeuOLD" is discouraged (0 uses).
New usage of "dfhnorm2" is discouraged (3 uses).
New usage of "dfich2OLD" is discouraged (0 uses).
New usage of "dfich2ai" is discouraged (1 uses).
Expand Down Expand Up @@ -15170,19 +15168,14 @@ New usage of "erngplus2-rN" is discouraged (0 uses).
New usage of "erngring-rN" is discouraged (0 uses).
New usage of "erngset-rN" is discouraged (3 uses).
New usage of "eu1OLD" is discouraged (0 uses).
New usage of "eu6OLD" is discouraged (0 uses).
New usage of "eu6OLDOLD" is discouraged (0 uses).
New usage of "euaeOLD" is discouraged (0 uses).
New usage of "euanvOLD" is discouraged (0 uses).
New usage of "eubiOLD" is discouraged (0 uses).
New usage of "eubidOLD" is discouraged (0 uses).
New usage of "eubiiOLD" is discouraged (0 uses).
New usage of "euequOLD" is discouraged (0 uses).
New usage of "euexALTOLD" is discouraged (0 uses).
New usage of "euexOLD" is discouraged (0 uses).
New usage of "euimOLD" is discouraged (0 uses).
New usage of "eujustALT" is discouraged (0 uses).
New usage of "eunexOLD" is discouraged (0 uses).
New usage of "euorvOLD" is discouraged (0 uses).
New usage of "ex-decpmul" is discouraged (0 uses).
New usage of "ex-gt" is discouraged (0 uses).
Expand Down Expand Up @@ -15217,8 +15210,6 @@ New usage of "exists2OLD" is discouraged (0 uses).
New usage of "exlimddOLD" is discouraged (0 uses).
New usage of "exlimexi" is discouraged (2 uses).
New usage of "exlimimddOLD" is discouraged (0 uses).
New usage of "exmoOLD" is discouraged (0 uses).
New usage of "exmoeuOLD" is discouraged (0 uses).
New usage of "expcomdg" is discouraged (0 uses).
New usage of "f1cofveqaeqALT" is discouraged (0 uses).
New usage of "f1oweALT" is discouraged (0 uses).
Expand Down Expand Up @@ -16331,13 +16322,11 @@ New usage of "mndomgmid" is discouraged (3 uses).
New usage of "mo3OLD" is discouraged (1 uses).
New usage of "mo4OLD" is discouraged (0 uses).
New usage of "mo4fOLD" is discouraged (0 uses).
New usage of "moabsOLD" is discouraged (0 uses).
New usage of "moanimvOLD" is discouraged (0 uses).
New usage of "mobiOLD" is discouraged (0 uses).
New usage of "mobidOLD" is discouraged (0 uses).
New usage of "mobidvALT" is discouraged (0 uses).
New usage of "mobiiOLD" is discouraged (0 uses).
New usage of "moeuOLD" is discouraged (0 uses).
New usage of "moimiOLD" is discouraged (0 uses).
New usage of "mpteq12dvOLD" is discouraged (0 uses).
New usage of "mptresidOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -17271,7 +17260,6 @@ New usage of "sb6fALT" is discouraged (1 uses).
New usage of "sb7fALT" is discouraged (1 uses).
New usage of "sbal1" is discouraged (1 uses).
New usage of "sbal2OLD" is discouraged (0 uses).
New usage of "sbal2OLDOLD" is discouraged (0 uses).
New usage of "sbalOLD" is discouraged (0 uses).
New usage of "sbanALT" is discouraged (1 uses).
New usage of "sbanOLD" is discouraged (0 uses).
Expand All @@ -17294,7 +17282,6 @@ New usage of "sbcel1vOLD" is discouraged (0 uses).
New usage of "sbcim2g" is discouraged (2 uses).
New usage of "sbcim2gVD" is discouraged (0 uses).
New usage of "sbco2ALT" is discouraged (1 uses).
New usage of "sbcom2OLD" is discouraged (0 uses).
New usage of "sbcoreleleq" is discouraged (2 uses).
New usage of "sbcoreleleqVD" is discouraged (0 uses).
New usage of "sbcrexgOLD" is discouraged (2 uses).
Expand Down Expand Up @@ -18231,7 +18218,6 @@ Proof modification of "cbvalvOLD" is discouraged (53 steps).
Proof modification of "cbveuALT" is discouraged (48 steps).
Proof modification of "cbvexsv" is discouraged (29 steps).
Proof modification of "cbvexvOLD" is discouraged (38 steps).
Proof modification of "cbvmoOLD" is discouraged (48 steps).
Proof modification of "cbvrabvOLD" is discouraged (19 steps).
Proof modification of "cbvrexdva2OLD" is discouraged (128 steps).
Proof modification of "ccat2s1fvwALT" is discouraged (149 steps).
Expand Down Expand Up @@ -18290,7 +18276,6 @@ Proof modification of "dedtOLD" is discouraged (19 steps).
Proof modification of "demoivreALT" is discouraged (1087 steps).
Proof modification of "dfbi1ALT" is discouraged (100 steps).
Proof modification of "dfeu" is discouraged (35 steps).
Proof modification of "dfeuOLD" is discouraged (33 steps).
Proof modification of "dfich2OLD" is discouraged (134 steps).
Proof modification of "dfich2ai" is discouraged (140 steps).
Proof modification of "dfich2bi" is discouraged (121 steps).
Expand Down Expand Up @@ -18552,19 +18537,14 @@ Proof modification of "equsexALT" is discouraged (37 steps).
Proof modification of "equsexvwOLD" is discouraged (36 steps).
Proof modification of "equviniOLD" is discouraged (68 steps).
Proof modification of "eu1OLD" is discouraged (86 steps).
Proof modification of "eu6OLD" is discouraged (52 steps).
Proof modification of "eu6OLDOLD" is discouraged (265 steps).
Proof modification of "euaeOLD" is discouraged (49 steps).
Proof modification of "euanvOLD" is discouraged (7 steps).
Proof modification of "eubiOLD" is discouraged (15 steps).
Proof modification of "eubidOLD" is discouraged (48 steps).
Proof modification of "eubiiOLD" is discouraged (17 steps).
Proof modification of "euequOLD" is discouraged (36 steps).
Proof modification of "euexALTOLD" is discouraged (32 steps).
Proof modification of "euexOLD" is discouraged (44 steps).
Proof modification of "euimOLD" is discouraged (37 steps).
Proof modification of "eujustALT" is discouraged (188 steps).
Proof modification of "eunexOLD" is discouraged (53 steps).
Proof modification of "euorvOLD" is discouraged (7 steps).
Proof modification of "ex-decpmul" is discouraged (304 steps).
Proof modification of "ex-natded5.13" is discouraged (67 steps).
Expand Down Expand Up @@ -18595,8 +18575,6 @@ Proof modification of "exists2OLD" is discouraged (61 steps).
Proof modification of "exlimddOLD" is discouraged (19 steps).
Proof modification of "exlimexi" is discouraged (15 steps).
Proof modification of "exlimimddOLD" is discouraged (13 steps).
Proof modification of "exmoOLD" is discouraged (22 steps).
Proof modification of "exmoeuOLD" is discouraged (39 steps).
Proof modification of "f1cofveqaeqALT" is discouraged (124 steps).
Proof modification of "f1oweALT" is discouraged (805 steps).
Proof modification of "f1rhm0to0ALT" is discouraged (161 steps).
Expand Down Expand Up @@ -18963,13 +18941,11 @@ Proof modification of "mndoissmgrpOLD" is discouraged (22 steps).
Proof modification of "mo3OLD" is discouraged (163 steps).
Proof modification of "mo4OLD" is discouraged (9 steps).
Proof modification of "mo4fOLD" is discouraged (54 steps).
Proof modification of "moabsOLD" is discouraged (28 steps).
Proof modification of "moanimvOLD" is discouraged (7 steps).
Proof modification of "mobiOLD" is discouraged (63 steps).
Proof modification of "mobidOLD" is discouraged (49 steps).
Proof modification of "mobidvALT" is discouraged (48 steps).
Proof modification of "mobiiOLD" is discouraged (17 steps).
Proof modification of "moeuOLD" is discouraged (52 steps).
Proof modification of "moimiOLD" is discouraged (17 steps).
Proof modification of "mpteq12dvOLD" is discouraged (18 steps).
Proof modification of "mptresidOLD" is discouraged (28 steps).
Expand Down Expand Up @@ -19231,7 +19207,6 @@ Proof modification of "sb6fALT" is discouraged (49 steps).
Proof modification of "sb7fALT" is discouraged (68 steps).
Proof modification of "sbal1" is discouraged (149 steps).
Proof modification of "sbal2OLD" is discouraged (157 steps).
Proof modification of "sbal2OLDOLD" is discouraged (157 steps).
Proof modification of "sbalOLD" is discouraged (49 steps).
Proof modification of "sbanALT" is discouraged (102 steps).
Proof modification of "sbanOLD" is discouraged (73 steps).
Expand All @@ -19256,7 +19231,6 @@ Proof modification of "sbcel1vOLD" is discouraged (48 steps).
Proof modification of "sbcim2g" is discouraged (83 steps).
Proof modification of "sbcim2gVD" is discouraged (139 steps).
Proof modification of "sbco2ALT" is discouraged (73 steps).
Proof modification of "sbcom2OLD" is discouraged (185 steps).
Proof modification of "sbcoreleleq" is discouraged (91 steps).
Proof modification of "sbcoreleleqVD" is discouraged (176 steps).
Proof modification of "sbcrexgOLD" is discouraged (77 steps).
Expand Down
125 changes: 0 additions & 125 deletions set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -19339,17 +19339,6 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
ZUOURUTBGHZDFHZTAKZDLBLZUQUTVBVATAKZBLDLVEDLBLVDADBFGMVEDBNVEVCBDVBVAAOUA
UBABDGFMUCUOUSUJDFAGCBPQUDUJFEDPUEUIUQULBGIUOUMUIUPULBGAFEDPQULGCBPUFUGUH
GCRSFERS $.

$( Obsolete version of ~ sbcom2 as of 23-Dec-2022. (Contributed by NM,
27-May-1997.) (Proof shortened by Wolf Lammen, 24-Sep-2018.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
sbcom2OLD $p |- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph ) $=
( vu vv weq wex wsb wb ax6ev wi wa wal 2sb6 alcom nfv sbequ sbbid ancomst
2albii 3bitri bitr4i syl5bbr sylan9bb sylan9bbr bitr3d ex exlimdv exlimiv
mp2 ) FCHZFIGEHZGIZABCJZDEJZADEJZBCJZKZFCLGELUMUOUTMFUMUNUTGUMUNUTUMUNNAD
GJZBFJZUQUSUMVBUPDGJZUNUQVBABFJZDGJZUMVCVEBFHZDGHZNAMZDOBOZVBVEVGVFNAMZBO
DOVJDOBOVIADBGFPVJDBQVJVHBDVGVFAUAUBUCABDFGPUDUMVDUPDGUMDRAFCBSTUEUPGEDSU
FUNVBURBFJUMUSUNVAURBFUNBRAGEDSTURFCBSUGUHUIUJUKUL $.
$}

${
Expand Down Expand Up @@ -22098,19 +22087,6 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
AACCHULUOACJACDCKLMNOUJULGZPUNUKUMSZCFZUPURUNUTIUJUMCDTOURUPUKASZBFZCFZUJ
UTURUPVACFZBFVCURUOVDBCDBQACDTRVABCUAUBUJVBUSCBCCQUJUKBUCVBUSIBCDUDUKABUE
UFRUGUHUI $.

$( Obsolete version of ~ sbal2 as of 24-Dec-2022. (Contributed by NM,
2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf
Lammen, 3-Oct-2018.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
sbal2OLDOLD $p |- ( -. A. x x = y ->
( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) ) $=
( weq wal wn wsb wb wa wi sb4b adantl nfnae albid alcom wnf drsb2 syl5bbr
sbid nfeqf1 19.21t syl syl5bb sylan9bbr bitr4d ex dral2 bitr3d pm2.61d2 )
BCEBFGZCDEZCFZABFZCDHZACDHZBFZIZUKUMGZURUKUSJUOULUNKZCFZUQUSUOVAIUKUNCDLM
USUQULAKZCFZBFZUKVAUSUPVCBCDBNACDLOVDVBBFZCFUKVAVBBCPUKVEUTCBCCNUKULBQVEU
TIBCDUAULABUBUCOUDUEUFUGUMUNUOUQUNUNCCHUMUOUNCTUNCDCRSAUPCDBAACCHUMUPACTA
CDCRSUHUIUJ $.
$}

${
Expand Down Expand Up @@ -23058,34 +23034,6 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
eu6im $p |- ( E. y A. x ( ph <-> x = y ) -> E! x ph ) $=
( vz weq wi wal wex wa wb weu exsbim anim1i eu6lem eu3v 3imtr4i ) BCEZAFB
GCHZABDEFBGDHZIABHZSIAQJBGCHABKRTSABCLMABCDNABDOP $.

$( Obsolete version of ~ eu6 as of 31-Dec-2022. Alternate definition of
the unique existential quantifier ~ df-eu not using the at-most-one
quantifier. (Contributed by NM, 12-Aug-1993.) This used to be the
definition of the unique existential quantifier, while ~ df-eu was then
proved as ~ dfeu . (Revised by BJ, 30-Sep-2022.) (Proof shortened by
Wolf Lammen, 3-Jan-2023.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
eu6OLD $p |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) ) $=
( vz wex weq wi wal wa weu wb exsb anbi1i eu3v eu6lem 3bitr4i ) ABEZABDFG
BHDEZIBCFZAGBHCEZRIABJASKBHCEQTRABCLMABDNABCDOP $.

$( Obsolete version of ~ eu6 as of 28-Dec-2022. (Contributed by NM,
12-Aug-1993.) This used to be the definition of the unique existential
quantifier, while ~ df-eu was then proved as ~ dfeu . (Revised by BJ,
30-Sep-2022.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
eu6OLDOLD $p |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) ) $=
( vz weu wex wmo wa weq wal anbi12i 19.26 albii anass bitri bicomi bitr3i
wi 3bitri exbii wb df-eu exsb df-mo pm3.33 pm4.71i equvelv equequ2 bicomd
exdistrv imbi2d albidv pm5.32ri anbi2i ancom anbi1i 19.42v ax6evr biantru
dfbi2 ) ABEABFZABGZHBCIZARZBJZCFZABDIZRZBJZDFZHZAVCUAZBJZCFZABUBVAVFVBVJA
BCUCABDUDKVKVMCDIZDFZHZCFZVNVKVEVIHZDFZCFVRVEVICDUJVTVQCVTVMVOHZDFVQVSWAD
VSVDVHHZBJZWAVDVHBLZWCWBVCVGRZHZBJWCWEBJZHZWAWBWFBWBWEVCAVGUEUFMWBWEBLWHV
SVOHZVEAVCRZBJZVOHZHZWAWCVSWGVOWDCDBUGKWIVEVIVOHZHWMVEVIVONWNWLVEVOVIWKVO
VHWJBVOVGVCAVOVCVGCDBUHUIUKULUMUNOWMVEWKHZVOHWAVEWKVONWOVMVOWOVDWJHZBJVMV
DWJBLWPVLBWPWJVDHZVLVDWJUOVLWQAVCUTPOMQUPQSSQTVMVODUQOTQVQVMCVMVQVPVMDCUR
USPTOS $.
$}

${
Expand Down Expand Up @@ -23291,54 +23239,6 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
ACDFZAGZCHBCDZQCCBIRPABCAJKLOACMN $.
$}

$( old theorems $)

$( Obsolete proof of ~ moeu as of 31-Dec-2022. (Contributed by NM,
8-Mar-1995.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
moeuOLD $p |- ( E* x ph <-> ( E. x ph -> E! x ph ) ) $=
( wmo wex wi wa weu ax-1 nexmo pm2.6 ax-mp impbii anclb df-eu bicomi imbi2i
wn 3bitri ) ABCZABDZSEZTTSFZETABGZESUASTHTQSEUASEABITSJKLTSMUBUCTUCUBABNOPR
$.

$( Obsolete proof of ~ exmo as of 31-Dec-2022. (Contributed by NM,
8-Mar-1995.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
exmoOLD $p |- ( E. x ph \/ E* x ph ) $=
( wex wmo wn weu wi pm2.21 moeu sylibr orri ) ABCZABDZLELABFZGMLNHABIJK $.

${
$d x y $. $d ph y $.
$( Obsolete proof of ~ euex as of 31-Dec-2022. (Contributed by NM,
15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof
shortened by Wolf Lammen, 4-Dec-2018.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
euexOLD $p |- ( E! x ph -> E. x ph ) $=
( vy weu weq wb wal wex wi ax6ev biimpr com12 eximii 19.35i exlimiv sylbi
eu6 ) ABDABCEZFZBGZCHABHZABCQTUACSABRSAIBBCJSRAARKLMNOP $.
$}

$( Obsolete proof of ~ dfeu as of 31-Dec-2022. (Contributed by NM,
23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
dfeuOLD $p |- ( E! x ph <-> ( E. x ph /\ E* x ph ) ) $=
( weu wex wmo wa euex eumo jca wi moeu biimpi impcom impbii ) ABCZABDZABEZF
OPQABGABHIQPOQPOJABKLMN $.

$( Obsolete proof of ~ moabs as of 31-Dec-2022. (Contributed by NM,
4-Nov-2002.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
moabsOLD $p |- ( E* x ph <-> ( E. x ph -> E* x ph ) ) $=
( wex weu wi wmo pm5.4 moeu imbi2i 3bitr4ri ) ABCZKABDZEZEMKABFZENKLGNMKABH
ZIOJ $.

$( Obsolete proof of ~ exmoeu as of 31-Dec-2022. (Contributed by NM,
5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
exmoeuOLD $p |- ( E. x ph <-> ( E* x ph -> E! x ph ) ) $=
( wex wmo weu wi moeu biimpi com12 exmo ori con1i euex ja impbii ) ABCZABDZ
ABEZFQPRQPRFABGHIQRPPQPQABJKLABMNO $.

$( substitution $)

${
Expand Down Expand Up @@ -23412,13 +23312,6 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
cbveuALT $p |- ( E! x ph <-> E! y ps ) $=
( wex wmo wa weu cbvex cbvmo anbi12i df-eu 3bitr4i ) ACHZACIZJBDHZBDIZJAC
KBDKQSRTABCDEFGLABCDEFGMNACOBDOP $.

$( Obsolete version of ~ cbvmo as of 4-Jan-2023. (Contributed by NM,
9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
cbvmoOLD $p |- ( E* x ph <-> E* y ps ) $=
( wex weu wi wmo cbvex cbveu imbi12i moeu 3bitr4i ) ACHZACIZJBDHZBDIZJACK
BDKQSRTABCDEFGLABCDEFGMNACOBDOP $.
$}

${
Expand Down Expand Up @@ -23459,16 +23352,6 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not
UEUFCUAUBUCUD $.
$}

${
$d x y $. $d ph y $.
$( Obsolete proof of ~ euex as of 31-Dec-2022. (Contributed by NM,
15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
euexALTOLD $p |- ( E! x ph -> E. x ph ) $=
( vy weu wsb weq wi wal wa wex nfv eu1 exsimpl sylbi ) ABDAABCEBCFGCHZIBJ
ABJABCACKLAOBMN $.
$}

${
euor.nf $e |- F/ x ph $.
$( Introduce a disjunct into a unique existential quantifier. For a
Expand Down Expand Up @@ -48030,14 +47913,6 @@ This theorem is proved directly from set theory axioms (no set theory
eunex $p |- ( E! x ph -> E. x -. ph ) $=
( vy weq wb wal wex wn weu dtru albi mtbiri exlimiv eu6 exnal 3imtr4i ) A
BCDZEBFZCGABFZHZABIAHBGRTCRSQBFBCJAQBKLMABCNABOP $.

$( Obsolete proof of ~ eunex as of 2-Jan-2023. (Contributed by NM,
24-Oct-2010.) (New usage is discouraged.)
(Proof modification is discouraged.) $)
eunexOLD $p |- ( E! x ph -> E. x -. ph ) $=
( vy wex weq wi wal wa wn weu dtru alim mtoi exlimiv adantl exnal 3imtr4i
eu3v ) ABDZABCEZFBGZCDZHABGZIZABJAIBDUBUDSUAUDCUAUCTBGBCKATBLMNOABCRABPQ
$.
$}

${
Expand Down

0 comments on commit 8de506c

Please sign in to comment.