diff --git a/discouraged b/discouraged index 53519d1697..45e6bb6351 100755 --- a/discouraged +++ b/discouraged @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). @@ -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). diff --git a/set.mm b/set.mm index 840e0f7fe1..ec97caf55e 100644 --- a/set.mm +++ b/set.mm @@ -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 $. $} ${ @@ -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 $. $} ${ @@ -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 $. $} ${ @@ -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 $) ${ @@ -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 $. $} ${ @@ -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 @@ -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 - $. $} ${