diff --git a/changes-set.txt b/changes-set.txt index 2e71a0701..cdf860cf1 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -80,7 +80,7 @@ proposed syl5ib imbitrid proposed syl5ibcom imbitridcom proposed syl5ibr imbitrrid proposed syl5ibrcom imbitrridcom -proposed syl5bb bitrid compare to bitri or bitrd +underway syl5bb bitrid compare to bitri or bitrd proposed syl6 imtrdi alternate proposal: syldi proposed syl6com imtrdicom proposed syl6d imtrdid diff --git a/set.mm b/set.mm index 552373cba..2eeba1829 100644 --- a/set.mm +++ b/set.mm @@ -2729,7 +2729,7 @@ intermediate steps that are essentially incomprehensible to humans (other biconditional from two biconditionals: ~ bitri , ~ bitr2i , ~ bitr3i , ~ bitr4i (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, - ~ syld , ~ syl5 , ~ syl6 , ~ mpbid , ~ bitrd , ~ syl5bb , ~ bitrdi and + ~ syld , ~ syl5 , ~ syl6 , ~ mpbid , ~ bitrd , ~ bitrid , ~ bitrdi and variants. (Contributed by BJ, 21-Apr-2019.) $) sylbbr $p |- ( ch -> ph ) $= ( biimpri sylibr ) CBABCEFDG $. @@ -3120,10 +3120,20 @@ intermediate steps that are essentially incomprehensible to humans (other $} ${ - syl5bb.1 $e |- ( ph <-> ps ) $. - syl5bb.2 $e |- ( ch -> ( ps <-> th ) ) $. + bitrid.1 $e |- ( ph <-> ps ) $. + bitrid.2 $e |- ( ch -> ( ps <-> th ) ) $. $( A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) $) + bitrid $p |- ( ch -> ( ph <-> th ) ) $= + ( wb a1i bitrd ) CABDABGCEHFI $. + $} + + ${ + syl5bb.1 $e |- ( ph <-> ps ) $. + syl5bb.2 $e |- ( ch -> ( ps <-> th ) ) $. + $( A syllogism inference from two biconditionals. This is in the process + of being renamed to ~ bitrid (New usages should use ~ bitrid ). + (Contributed by NM, 12-Mar-1993.) $) syl5bb $p |- ( ch -> ( ph <-> th ) ) $= ( wb a1i bitrd ) CABDABGCEHFI $. $} @@ -3134,7 +3144,7 @@ intermediate steps that are essentially incomprehensible to humans (other $( A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) $) bitr2id $p |- ( ch -> ( th <-> ph ) ) $= - ( syl5bb bicomd ) CADABCDEFGH $. + ( bitrid bicomd ) CADABCDEFGH $. $} ${ @@ -3143,7 +3153,7 @@ intermediate steps that are essentially incomprehensible to humans (other $( A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) $) bitr3id $p |- ( ch -> ( ph <-> th ) ) $= - ( bicomi syl5bb ) ABCDBAEGFH $. + ( bicomi bitrid ) ABCDBAEGFH $. $} ${ @@ -3393,7 +3403,7 @@ intermediate steps that are essentially incomprehensible to humans (other $( More general version of ~ 3bitr4i . Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.) $) 3bitr4g $p |- ( ph -> ( th <-> ta ) ) $= - ( syl5bb bitr4di ) ADCEDBACGFIHJ $. + ( bitrid bitr4di ) ADCEDBACGFIHJ $. $} $( Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. @@ -3992,7 +4002,7 @@ the conclusion alone (see ~ pm5.1im and ~ pm5.21im ). (Contributed by Lammen, 14-Sep-2013.) $) imim21b $p |- ( ( ps -> ph ) -> ( ( ( ph -> ch ) -> ( ps -> th ) ) <-> ( ps -> ( ch -> th ) ) ) ) $= - ( wi bi2.04 wb pm5.5 imbi1d imim2i pm5.74d syl5bb ) ACEZBDEEBMDEZEBAEZBCDEZ + ( wi bi2.04 wb pm5.5 imbi1d imim2i pm5.74d bitrid ) ACEZBDEEBMDEZEBAEZBCDEZ EMBDFOBNPANPGBAMCDACHIJKL $. @@ -8871,7 +8881,7 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of ~ dedlemb . (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.) $) ifpfal $p |- ( -. ph -> ( if- ( ph , ps , ch ) <-> ch ) ) $= - ( wif wn ifpn ifptru syl5bb ) ABCDAEZCBDICABCFICBGH $. + ( wif wn ifpn ifptru bitrid ) ABCDAEZCBDICABCFICBGH $. $( Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of @@ -11920,7 +11930,7 @@ Principia Mathematica (1927), Russell and Whitehead used the Sheffer 29-Oct-2023.) (Proof shortened by Wolf Lammen, 17-Dec-2023.) $) norass $p |- ( ( ph <-> ch ) <-> ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) ) $= - ( wnor wo wb wn notbi wi norasslem1 bibi12i bicom norasslem2 bibi12d syl5bb + ( wnor wo wb wn notbi wi norasslem1 bibi12i bicom norasslem2 bibi12d bitrid impimprbi norasslem3 pm2.61i 3bitr4i df-nor norcom orbi1i orcom ) ABDZCEZAB CDZEZFZUEGZUGGZFACFZUDCDZAUFDZFUEUGHBAECIZBCEAIZFZBADZCEZUFAEZFUKUHUNURUOUS BACJBCAJKBUKUPFUKCAFBUPACLBCUNAUOBCAMBACMNOUKACIZCAIZFBGZUPACPVBUTUNVAUOBAC @@ -12818,7 +12828,7 @@ the logical conjunction ( ~ df-an ). Carneiro, 8-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) $) cad0OLD $p |- ( -. ch -> ( cadd ( ph , ps , ch ) <-> ( ph /\ ps ) ) ) $= - ( wcad wa wxo wo wn df-cad idd pm2.21 adantrd jaod orc impbid1 syl5bb ) ABC + ( wcad wa wxo wo wn df-cad idd pm2.21 adantrd jaod orc impbid1 bitrid ) ABC DABEZCABFZEZGZCHZQABCIUATQUAQQSUAQJUACQRCQKLMQSNOP $. $( The value of the carry is, if the input carry is true, the disjunction, @@ -18211,7 +18221,7 @@ in which (1) there are no wff metavariables and (2) all setvar variables ax12wdemo $p |- ( x = y -> ( A. y ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) -> A. x ( x = y -> ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) ) ) ) $= - ( vw vv wel wal w3a weq elequ1 elequ2 cbvalvw a1i albidv syl5bb 3anbi123d + ( vw vv wel wal w3a weq elequ1 elequ2 cbvalvw a1i albidv bitrid 3anbi123d wb 3anbi13d ax12w ) ABFZCAFZAGZBAFZCGZBGZHBBFZCDFZDGZEBFZCGZEGZHAEFZUBEAF ZCGZEGZHABEABIZTUFUBUHUEUKABBJUBUHQUPUAUGADADCKLMUEUOUPUKUDUNBEBEIZUCUMCB EAJNLZUPUNUJEUPUMUICABEKNNOPUQTULUEUOUBBEAKUEUOQUQURMRS $. @@ -22867,7 +22877,7 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not eu6lem $p |- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) ) $= ( weq wb wal wex wi wa 19.42v alsyl equvelv sylib pm4.71i albiim biancomi - equequ2 imbi2d exbii albidv anbi2d syl5bb pm5.32ri bitr4i ax6evr 3bitr4ri + equequ2 imbi2d exbii albidv anbi2d bitrid pm5.32ri bitr4i ax6evr 3bitr4ri biantru exdistrv bitri ) ABCEZFBGZCHUKAIBGZABDEZIZBGZJZDHZCHUMCHUPDHJULUR CULCDEZJZDHULUSDHZJURULULUSDKUQUTDUQUQUSJUTUQUSUQUKUNIBGUSUKAUNBLCDBMNOUS ULUQULUMAUKIZBGZJUSUQULUMVCAUKBPQUSVCUPUMUSVBUOBUSUKUNACDBRSUAUBUCUDUETVA @@ -25968,7 +25978,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication use of ~ cleqh ). (Revised by BJ, 23-Jun-2019.) $) abbi $p |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) $= ( vy cab wceq cv wcel wal dfcleq nfsab1 nfbi nfv weq wsb df-clab sbequ12r - wb syl5bb bibi12d cbvalv1 bitr2i ) ACEZBCEZFDGZUCHZUEUDHZRZDIABRZCIDUCUDJ + wb bitrid bibi12d cbvalv1 bitr2i ) ACEZBCEZFDGZUCHZUEUDHZRZDIABRZCIDUCUDJ UHUIDCUFUGCACDKBCDKLUIDMDCNZUFAUGBUFACDOUJAADCPADCQSUGBCDOUJBBDCPBDCQSTUA UB $. $( $j usage 'abbi' avoids 'ax-8' 'df-clel' ; $) @@ -27688,7 +27698,7 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.) $) necon3abid $p |- ( ph -> ( A =/= B <-> -. ps ) ) $= - ( wne wceq wn df-ne notbid syl5bb ) CDFCDGZHABHCDIALBEJK $. + ( wne wceq wn df-ne notbid bitrid ) CDFCDGZHABHCDIALBEJK $. $} ${ @@ -27752,7 +27762,7 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) $) necon3bid $p |- ( ph -> ( A =/= B <-> C =/= D ) ) $= - ( wne wceq wn df-ne necon3bbid syl5bb ) BCGBCHZIADEGBCJAMDEFKL $. + ( wne wceq wn df-ne necon3bbid bitrid ) BCGBCHZIADEGBCJAMDEFKL $. $} ${ @@ -32202,7 +32212,7 @@ general is seen either by substitution (when the variable ` V ` has no 21-Jun-2013.) Avoid ~ ax-9 , ~ ax-12 , ~ ax-ext . (Revised by SN, 8-Sep-2024.) $) ceqsralv $p |- ( A e. B -> ( A. x e. B ( x = A -> ph ) <-> ps ) ) $= - ( cv wceq wi wral wcel pm5.74i ralbii wrex r19.23v wb risset pm5.5 syl5bb + ( cv wceq wi wral wcel pm5.74i ralbii wrex r19.23v wb risset pm5.5 bitrid sylbi ) CGDHZAIZCEJUABIZCEJZDEKZBUBUCCEUAABFLMUDUACENZBIZUEBUABCEOUEUFUGB PCDEQUFBRTSS $. $( $j usage 'ceqsralv' avoids 'ax-9' 'ax-12' 'ax-ext'; $) @@ -33572,7 +33582,7 @@ general is seen either by substitution (when the variable ` V ` has no $( Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015.) $) ralxpxfr2d $p |- ( ph -> ( A. x e. B ps <-> A. y e. C A. z e. D ch ) ) $= - ( wral wi wal wrex albidv ralcom4 ralbii wceq df-ral imbi1d syl5bb bitr2i + ( wral wi wal wrex albidv ralcom4 ralbii wceq df-ral imbi1d bitrid bitr2i wcel r19.23v albii 3bitr4ri bitrdi pm5.74da biidd ceqsalv 2ralbidv bitrd cv ) ABDHNZDUPZGUAZBOZDPZFJNZEINZCFJNEINAUQUSFJQZEIQZBOZDPZVCUQURHUFZBOZD PAVGBDHUBAVIVFDAVHVEBLUCRUDUTFJNZDPZEINVJEINZDPVCVGVJEDISVBVKEIUTFDJSTVFV @@ -33682,7 +33692,7 @@ general is seen either by substitution (when the variable ` V ` has no substitution. (Contributed by NM, 30-Apr-2004.) $) ceqsrexv $p |- ( A e. B -> ( E. x e. B ( x = A /\ ph ) <-> ps ) ) $= ( cv wceq wa wrex wcel wex df-rex an12 exbii bitr4i eleq1 anbi12d bianabs - ceqsexgv syl5bb ) CGZDHZAIZCEJZUCUBEKZAIZIZCLZDEKZBUEUFUDIZCLUIUDCEMUHUKC + ceqsexgv bitrid ) CGZDHZAIZCEJZUCUBEKZAIZIZCLZDEKZBUEUFUDIZCLUIUDCEMUHUKC UCUFANOPUJUIBUGUJBICDEUCUFUJABUBDEQFRTSUA $. $( Elimination of a restricted existential quantifier, using implicit @@ -33702,7 +33712,7 @@ general is seen either by substitution (when the variable ` V ` has no ceqsrex2v $p |- ( ( A e. C /\ B e. D ) -> ( E. x e. C E. y e. D ( ( x = A /\ y = B ) /\ ph ) <-> ch ) ) $= ( wcel cv wceq wa wrex anass rexbii r19.42v ceqsrexv bitri anbi2d rexbidv - syl5bb sylan9bb ) FHLZDMFNZEMGNZOAOZEIPZDHPZUHBOZEIPZGILCUKUGUHAOZEIPZOZD + bitrid sylan9bb ) FHLZDMFNZEMGNZOAOZEIPZDHPZUHBOZEIPZGILCUKUGUHAOZEIPZOZD HPUFUMUJUPDHUJUGUNOZEIPUPUIUQEIUGUHAQRUGUNEISUARUOUMDFHUGUNULEIUGABUHJUBU CTUDBCEGIKTUE $. $} @@ -33925,7 +33935,7 @@ general is seen either by substitution (when the variable ` V ` has no ~ ax-12 . (Revised by SN, 5-Oct-2024.) $) elabg $p |- ( A e. V -> ( A e. { x | ph } <-> ps ) ) $= ( wcel cab cv wceq wi wal elab6g wex pm5.74i albii 19.23v bitri elisset - wb pm5.5 syl syl5bb bitrd ) DEGZDACHGCIDJZAKZCLZBACDEMUHUFCNZBKZUEBUHUFBK + wb pm5.5 syl bitrid bitrd ) DEGZDACHGCIDJZAKZCLZBACDEMUHUFCNZBKZUEBUHUFBK ZCLUJUGUKCUFABFOPUFBCQRUEUIUJBTCDESUIBUAUBUCUD $. $( $j usage 'elabg' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) @@ -33963,7 +33973,7 @@ general is seen either by substitution (when the variable ` V ` has no $( Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) $) elab2g $p |- ( A e. V -> ( A e. B <-> ps ) ) $= - ( wcel cab eleq2i elabg syl5bb ) DEIDACJZIDFIBENDHKABCDFGLM $. + ( wcel cab eleq2i elabg bitrid ) DEIDACJZIDFIBENDHKABCDFGLM $. $} ${ @@ -34064,7 +34074,7 @@ general is seen either by substitution (when the variable ` V ` has no distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) $) elrabf $p |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) ) $= ( crab wcel cvv wa elex adantr cv cab df-rab eleq2i nfel nfan wceq elabgf - eleq1 anbi12d syl5bb pm5.21nii ) DACEJZKZDLKZDEKZBMZDUHNUKUJBDENOUIDCPZEK + eleq1 anbi12d bitrid pm5.21nii ) DACEJZKZDLKZDEKZBMZDUHNUKUJBDENOUIDCPZEK ZAMZCQZKUJULUHUPDACERSUOULCDLFUKBCCDEFGTHUAUMDUBUNUKABUMDEUDIUEUCUFUG $. $} @@ -34098,7 +34108,7 @@ general is seen either by substitution (when the variable ` V ` has no ( A e. { x e. B | ph } <-> ps ) ) $= ( crab wcel cv wa cab wceq wb wi wal df-rab eleq2i id nfa1 nfv nfan eleq1 sp biimparc biantrurd bibi1d pm5.74da syl5ibcom imp alrimi elabgt syl2an2 - syl5bb ) DACEFZGDCHZEGZAIZCJZGZUNDKZABLZMZCNZDEGZIZBUMUQDACEOPVCVCVBUSUPB + bitrid ) DACEFZGDCHZEGZAIZCJZGZUNDKZABLZMZCNZDEGZIZBUMUQDACEOPVCVCVBUSUPB LZMZCNURBLVCQVDVFCVBVCCVACRVCCSTVBVCVFVBVAVCVFVACUBVCUSUTVEVCUSIZAUPBVGUO AUSUOVCUNDEUAUCUDUEUFUGUHUIUPBCDEUJUKUL $. $} @@ -34327,7 +34337,7 @@ general is seen either by substitution (when the variable ` V ` has no by NM, 5-Apr-1995.) $) eueq2 $p |- E! x ( ( ph /\ x = A ) \/ ( -. ph /\ x = B ) ) $= ( cv wceq wa wn weu eueqi euanv biimpri mpan2 euorv bianfd eubidv mpbid - wo notnot syl2anc orcom orbi2d syl5bb mpdan id orbi1d pm2.61i ) AABGZCHZI + wo notnot syl2anc orcom orbi2d bitrid mpdan id orbi1d pm2.61i ) AABGZCHZI ZAJZUJDHZIZTZBKZAUMULTZBKZUQAUMJULBKZUSAUAZAUKBKZUTBCELUTAVBIAUKBMNOUMULB PUBAURUPBURULUMTAUPUMULUCAUMUOULAUMUNVAQUDUERSUMAUOTZBKZUQUMUOBKZVDUMUNBK ZVEBDFLVEUMVFIUMUNBMNOAUOBPUFUMVCUPBUMAULUOUMAUKUMUGQUHRSUI $. @@ -34585,7 +34595,7 @@ general is seen either by substitution (when the variable ` V ` has no Carneiro, 2-Oct-2015.) $) eqreu $p |- ( ( B e. A /\ ps /\ A. x e. A ( ph -> x = B ) ) -> E! x e. A ph ) $= - ( wcel cv wceq wi wral wreu wa wb ralbiim ceqsralv anbi2d syl5bb reu6i ex + ( wcel cv wceq wi wral wreu wa wb ralbiim ceqsralv anbi2d bitrid reu6i ex sylbird 3impib 3com23 ) EDGZACHEIZJCDKZBACDLZUDUFBUGUDUFBMZAUENCDKZUGUIUF UEAJCDKZMUDUHAUECDOUDUJBUFABCEDFPQRUDUIUGACDESTUAUBUC $. $} @@ -34624,7 +34634,7 @@ general is seen either by substitution (when the variable ` V ` has no 24-Oct-2006.) $) reu8 $p |- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) ) $= - ( wreu weq wb wral wrex wi wa cbvreuvw reu6 cv wcel ralbii wal syl5bb a1i + ( wreu weq wb wral wrex wi wa cbvreuvw reu6 cv wcel ralbii wal bitrid a1i dfbi2 r19.26 ancom equcom imbi2i biimt df-ral bi2.04 albii eleq1w imbi12d bicomd equcoms equsalvw 3bitrri bitrdi anbi12d bitr4id rexbiia 3bitri ) A CEGBDEGBDCHZIZDEJZCEKABCDHZLZDEJZMZCEKABCDEFNBDCEOVDVHCEVDBVBLZVBBLZMZDEJ @@ -35276,7 +35286,7 @@ too large (beyond the size of those used in standard mathematics), the (Proof modification is discouraged.) $) ru $p |- { x | x e/ x } e/ _V $= ( vy cv wnel cab cvv wcel wceq wex wel wb wn pm5.19 eleq1w df-nel eleq12d - wal id notbid mtbir syl5bb bibi12d spvv mto abeq2 nex isset nelir ) ACZUI + wal id notbid mtbir bitrid bibi12d spvv mto abeq2 nex isset nelir ) ACZUI DZAEZFUKFGBCZUKHZBIUMBUMABJZUJKZAQZUPBBJZUQLZKZUQMUOUSABUIULHZUNUQUJURABU LNUJAAJZLUTURUIUIOUTVAUQUTUIULUIULUTRZVBPSUAUBUCUDUJAULUETUFBUKUGTUH $. $( $j usage 'ru' avoids 'ax-13' 'ax-reg'; $) @@ -35634,7 +35644,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use 11-Oct-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by SN, 5-Oct-2024.) $) sbc6g $p |- ( A e. V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) $= - ( wsbc cab wcel cv wceq wi wal df-sbc elab6g syl5bb ) ABCECABFGCDGBHCIAJB + ( wsbc cab wcel cv wceq wi wal df-sbc elab6g bitrid ) ABCECABFGCDGBHCIAJB KABCLABCDMN $. $( Obsolete version of ~ sbc6g as of 5-Oct-2024. (Contributed by NM, @@ -35753,7 +35763,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use (Contributed by NM, 10-Nov-2005.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino Giotto, 12-Oct-2024.) $) sbcieg $p |- ( A e. V -> ( [. A / x ]. ph <-> ps ) ) $= - ( wsbc cab wcel df-sbc elabg syl5bb ) ACDGDACHIDEIBACDJABCDEFKL $. + ( wsbc cab wcel df-sbc elabg bitrid ) ACDGDACHIDEIBACDJABCDEFKL $. $( $j usage 'sbcieg' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} @@ -35808,7 +35818,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use deduction form. (Contributed by NM, 13-Dec-2014.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino Giotto, 12-Oct-2024.) $) sbcied $p |- ( ph -> ( [. A / x ]. ps <-> ch ) ) $= - ( wsbc cab wcel df-sbc elabd3 syl5bb ) BDEIEBDJKACBDELABCDEFGHMN $. + ( wsbc cab wcel df-sbc elabd3 bitrid ) BDEIEBDJKACBDELABCDEFGHMN $. $( $j usage 'sbcied' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} @@ -36259,7 +36269,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) ) $= ( vz wral wsbc cv wcel wnfc wa sbccow simpl wsb wceq sbsbc nfcv wb nfralw nfs1v weq sbequ12 ralbidv sbiev bitr3i nfnfc1 nfcvd id nfeqd nfan1 adantl - dfsbcq2 ralbid adantll syl5bb sbcied bitr3id ) ACEHZBDIUTBGJZIZGDIDFKZCDL + dfsbcq2 ralbid adantll bitrid sbcied bitr3id ) ACEHZBDIUTBGJZIZGDIDFKZCDL ZMZABDIZCEHZUTBGDNVEVBVGGDFVCVDOVBABGPZCEHZVEVADQZMVGVBUTBGPVIUTBGRUTVIBG VHBCEBESABGUBUABGUCAVHCEABGUDUEUFUGVDVJVIVGTVCVDVJMVHVFCEVDVJCCDUHVDCVADV DCVAUIVDUJUKULVJVHVFTVDABGDUNUMUOUPUQURUS $. @@ -36328,7 +36338,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use NM, 5-Nov-2005.) $) sbcabel $p |- ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) ) $= - ( vw wcel cvv cab wsbc wb cv wceq wa wex wal syl5bb abeq2 elex sbcan sbcg + ( vw wcel cvv cab wsbc wb cv wceq wa wex wal bitrid abeq2 elex sbcan sbcg sbcex2 sbcal sbcbig bibi1d bitrd albidv sbcbii 3bitr4g nfcri sbcgf exbidv anbi12d dfclel syl ) DFIDJIZACKZEIZBDLZABDLZCKZEIZMDFUAURHNZUSOZVEEIZPZHQ ZBDLZVEVCOZVGPZHQZVAVDVJVHBDLZHQURVMVHHBDUDURVNVLHVNVFBDLZVGBDLZPURVLVFVG @@ -38136,7 +38146,7 @@ technically classes despite morally (and provably) being sets, like ` 1 ` Gino Giotto, 28-Jun-2024.) $) ss2abdv $p |- ( ph -> { x | ps } C_ { x | ch } ) $= ( vy vz cab cin wceq wss cv wcel wa df-in wsb df-clab bicomi sbequ wi weq - anbi12i abbii anbi12d sbievw ax-1 impd sbimdv ancld impbid syl5bb 3bitr4g + anbi12i abbii anbi12d sbievw ax-1 impd sbimdv ancld impbid bitrid 3bitr4g a1i eqrdv eqtr3id eqtrid df-ss sylibr ) ABDHZCDHZIZUSJUSUTKAVAFLZUSMZVBUT MZNZFHZUSFUSUTOAVFBDFPZCDFPZNZFHZUSVIVEFVGVCVHVDVCVGBFDQRVDVHCFDQRUBUCAGV JUSAVIFGPZBDGPZGLZVJMVMUSMVKVLCDGPZNZAVLVIVOFGFGUAVGVLVHVNBFGDSCFGDSUDUEA @@ -39895,7 +39905,7 @@ technically classes despite morally (and provably) being sets, like ` 1 ` 10-Jun-2021.) $) rcompleq $p |- ( ( A C_ C /\ B C_ C ) -> ( A = B <-> ( C \ A ) = ( C \ B ) ) ) $= - ( wss wa cdif wceq ancom wb sscon34b ancoms anbi12d syl5bb eqss 3bitr4g ) A + ( wss wa cdif wceq ancom wb sscon34b ancoms anbi12d bitrid eqss 3bitr4g ) A CDZBCDZEZABDZBADZEZCAFZCBFZDZUCUBDZEZABGUBUCGUATSERUFSTHRTUDSUEQPTUDIBACJKA BCJLMABNUBUCNO $. @@ -40922,7 +40932,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, 10-Nov-2005.) $) sbcel1g $p |- ( A e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. C ) ) $= - ( wcel wsbc csb sbcel12 csbconstg eleq2d syl5bb ) CDFABGABCHZABDHZFBEFZMD + ( wcel wsbc csb sbcel12 csbconstg eleq2d bitrid ) CDFABGABCHZABDHZFBEFZMD FABCDIONDMABDEJKL $. $( Move proper substitution to first argument of an equality. (Contributed @@ -40938,7 +40948,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, $( Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) $) sbcel2 $p |- ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C ) $= - ( cvv wcel wsbc wb sbcel12 csbconstg eleq1d syl5bb wn sbcex con3i c0 noel + ( cvv wcel wsbc wb sbcel12 csbconstg eleq1d bitrid wn sbcex con3i c0 noel csb csbprc eleq2d mtbiri 2falsed pm2.61i ) BEFZCDFZABGZCABDRZFZHUFABCRZUG FUDUHABCDIUDUICUGABCEJKLUDMZUFUHUFUDUEABNOUJUHCPFCQUJUGPCABDSTUAUBUC $. @@ -40986,7 +40996,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, csbnestgfw $p |- ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C ) $= ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb abeq2i wb nfcr - sbcbii wnf alimi sbcnestgfw sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZ + sbcbii wnf alimi sbcnestgfw sylan2 bitrid abbidv sylan 3eqtr4g ) CFHZAEIZ BJZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVB GURUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUDZBJVGVBUAUMVHBAGEUBUEUTABCDP UFUGUHUIUJAGCUPSBGVAESUK $. @@ -41055,7 +41065,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, csbnestgf $p |- ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C ) $= ( vz wcel wnfc wal wa cv csb wsbc cab cvv wceq elex df-csb abeq2i wb nfcr - sbcbii wnf alimi sbcnestgf sylan2 syl5bb abbidv sylan 3eqtr4g ) CFHZAEIZB + sbcbii wnf alimi sbcnestgf sylan2 bitrid abbidv sylan 3eqtr4g ) CFHZAEIZB JZKGLZBDEMZHZACNZGOZUOEHZBACDMZNZGOZACUPMBVAEMULCPHZUNUSVCQCFRVDUNKZURVBG URUTBDNZACNZVEVBUQVFACVFGUPBGDESTUCUNVDUTAUDZBJVGVBUAUMVHBAGEUBUEUTABCDPU FUGUHUIUJAGCUPSBGVAESUK $. @@ -41156,7 +41166,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, $( Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.) $) sbccsb2 $p |- ( [. A / x ]. ph <-> A e. [_ A / x ]_ { x | ph } ) $= - ( wsbc cvv wcel cab sbcex elex cv abid sbcbii sbcel12 csbvarg eleq1d syl5bb + ( wsbc cvv wcel cab sbcex elex cv abid sbcbii sbcel12 csbvarg eleq1d bitrid csb bitr3id pm5.21nii ) ABCDZCEFZCBCABGZQZFZABCHCUCITBJZUBFZBCDZUAUDUFABCAB KLUGBCUEQZUCFUAUDBCUEUBMUAUHCUCBCENOPRS $. @@ -41251,7 +41261,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, (Contributed by AV, 20-Jun-2023.) $) 2nreu $p |- ( ( A e. X /\ B e. X /\ A =/= B ) -> ( ( ps /\ ch ) -> -. E! x e. X ph ) ) $= - ( vy wne wa wn wrex wsbc wb sbcan anbi12d syl5bb csb wcel w3a wreu wsb wi + ( vy wne wa wn wrex wsbc wb sbcan anbi12d bitrid csb wcel w3a wreu wsb wi weq wo cv simpl1 simpl2 simprl sbcieg 3ad2ant2 biimprd adantld imp simpl3 jca simp1 simp2 simp3 nfs1v sbcgf sbcne12 csbvarg csbconstg 3ad2ant1 sbcg neeq12d sbcbidv sbsbc sbcbii sbccow mpbird rspesbca syl2anc sbcrex sylibr @@ -41408,7 +41418,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, $( A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.) $) disjpss $p |- ( ( ( A i^i B ) = (/) /\ B =/= (/) ) -> A C. ( A u. B ) ) $= - ( cin c0 wceq wne wa wss wn cun wpss ssid biantru bitri sseq2 syl5bb syl6bi + ( cin c0 wceq wne wa wss wn cun wpss ssid biantru bitri sseq2 bitrid syl6bi ssin ss0 necon3ad imp nsspssun uncom psseq2i sylib ) ABCZDEZBDFZGBAHZIZAABJ ZKZUGUHUJUGUIBDUGUIBDHZBDEUIBUFHZUGUMUIUIBBHZGUNUOUIBLMBABRNUFDBOPBSQTUAUJA BAJZKULBAUBUPUKABAUCUDNUE $. @@ -41923,7 +41933,7 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of sbcssg $p |- ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) ) $= ( vy wcel cv wi wal wsbc csb wss sbcal sbcimg sbcel2 imbi12i bitrdi dfss2 - albidv syl5bb sbcbii 3bitr4g ) BEGZFHZCGZUEDGZIZFJZABKZUEABCLZGZUEABDLZGZ + albidv bitrid sbcbii 3bitr4g ) BEGZFHZCGZUEDGZIZFJZABKZUEABCLZGZUEABDLZGZ IZFJZCDMZABKUKUMMUJUHABKZFJUDUPUHFABNUDURUOFUDURUFABKZUGABKZIUOUFUGABEOUS ULUTUNABUECPABUEDPQRTUAUQUIABFCDSUBFUKUMSUC $. $} @@ -41956,7 +41966,7 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) $= ( c0 wne wa wrex wreu weq wi wral wb a1i bitri r19.26 adantr reu3 anbi12i an4 rexcom anbi2i anidm cv wcel nfra1 r19.3rz bicomd anbi2d ralbii bitr4d - jcab bitr2id ad2antlr ralcom anbi12d syl5bb ralbidv r19.23v 2ralbii wn wo + jcab bitr2id ad2antlr ralcom anbi12d bitrid ralbidv r19.23v 2ralbii wn wo wceq neneq anim12i olcd dfbi3 sylibr nfv nfim raaan2 syl 3bitrd 2rexbidva nfre1 reeanv bitr2di ) FHIZGHIZJZACGKZBFLZABFKZCGLZJZWDBFKZWDBDMZNZBFOZDF KZJZWFCGKZWFCEMZNZCGOZEGKZJZJZWIWOJZWMWSJZJZWIAWJWPJNZCGOZBFOZEGKDFKZJWHX @@ -43456,7 +43466,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). $( Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) $) rexsngf $p |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) $= - ( csn wrex wsbc wcel rexsns sbciegf syl5bb ) ACDHIACDJDEKBACDLABCDEFGMN + ( csn wrex wsbc wcel rexsns sbciegf bitrid ) ACDHIACDJDEKBACDLABCDEFGMN $. $( Restricted universal quantification over a singleton. (Contributed by @@ -43471,7 +43481,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). reusngf $p |- ( A e. V -> ( E! x e. { A } ph <-> ps ) ) $= ( vc vw csn wreu cv wsbc wi wral wa nfsbc1v dfsbcq wceq nfv weq wrex wcel sbceq1a reu8nf nfcv nfim nfralw nfan eqeq1 imbi2d ralbidv anbi12d rexsngf - eqeq2 imbi12d ralsngf anbi2d eqidd biantru bitr4di bitrd syl5bb ) ACDJZKA + eqeq2 imbi12d ralsngf anbi2d eqidd biantru bitr4di bitrd bitrid ) ACDJZKA ACHLZMZCHUAZNZHVDOZPZCVDUBZDEUCZBAVFACILZMCHIVDACVEQZACVMQACVMUDACVMVERUE VLVKBVFDVESZNZHVDOZPZBVJVRCDEBVQCFVPCHVDCVDUFVFVOCVNVOCTUGUHUICLZDSZABVIV QGVTVHVPHVDVTVGVOVFVSDVEUJUKULUMUNVLVRBACDMZDDSZNZPBVLVQWCBVPWCHDEWCHTVED @@ -43487,7 +43497,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). 30-Sep-2024.) $) ralsng $p |- ( A e. V -> ( A. x e. { A } ph <-> ps ) ) $= ( csn wral cv wceq wi wal wcel df-ral velsn imbi1i albii bitri wb a1i wex - elisset pm5.74i 19.23v pm5.5 3bitrd syl syl5bb ) ACDGZHZCIZDJZAKZCLZDEMZB + elisset pm5.74i 19.23v pm5.5 3bitrd syl bitrid ) ACDGZHZCIZDJZAKZCLZDEMZB UJUKUIMZAKZCLUNACUINUQUMCUPULACDOPQRUOULCUAZUNBSCDEUBURUNULBKZCLZURBKZBUN UTSURUMUSCULABFUCQTUTVASURULBCUDTURBUEUFUGUH $. $( $j usage 'ralsng' avoids 'ax-10' 'ax-11' 'ax-12'; $) @@ -43496,7 +43506,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). NM, 29-Jan-2012.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino Giotto, 30-Sep-2024.) $) rexsng $p |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) $= - ( wcel wn wral wb wrex cv wceq notbid ralsng dfrex2 bicom1 con1bid syl5bb + ( wcel wn wral wb wrex cv wceq notbid ralsng dfrex2 bicom1 con1bid bitrid csn syl ) DEGAHZCDTZIZBHZJZACUCKZBJUBUECDECLDMABFNOUGUDHUFBACUCPUFBUDUDUE QRSUA $. $( $j usage 'rexsng' avoids 'ax-10' 'ax-11' 'ax-12'; $) @@ -43663,7 +43673,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). 8-Apr-2023.) $) ralprgf $p |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) ) $= - ( cpr wral csn wa wcel cun df-pr ralsngf raleqi ralunb bi2anan9 syl5bb + ( cpr wral csn wa wcel cun df-pr ralsngf raleqi ralunb bi2anan9 bitrid bitri ) ADEFMZNZADEOZNZADFOZNZPZEGQZFHQZPBCPUGADUHUJRZNULADUFUOEFSUAADUHU JUBUEUMUIBUNUKCABDEGIKTACDFHJLTUCUD $. @@ -43674,7 +43684,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). rexprgf $p |- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) ) $= ( cpr wrex csn wo wcel wa cun rexsngf df-pr rexeqi orbi1d orbi2d sylan9bb - rexun bitri syl5bb ) ADEFMZNZADEOZNZADFOZNZPZEGQZFHQZRBCPZUJADUKUMSZNUOAD + rexun bitri bitrid ) ADEFMZNZADEOZNZADFOZNZPZEGQZFHQZRBCPZUJADUKUMSZNUOAD UIUSEFUAUBADUKUMUFUGUPUOBUNPUQURUPULBUNABDEGIKTUCUQUNCBACDFHJLTUDUEUH $. $} @@ -43688,7 +43698,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). Giotto, 30-Sep-2024.) $) ralprg $p |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) ) $= - ( cpr wral csn wa wcel cun df-pr raleqi ralunb ralsng bi2anan9 syl5bb + ( cpr wral csn wa wcel cun df-pr raleqi ralunb ralsng bi2anan9 bitrid bitri ) ADEFKZLZADEMZLZADFMZLZNZEGOZFHOZNBCNUEADUFUHPZLUJADUDUMEFQRADUFUH SUCUKUGBULUICABDEGITACDFHJTUAUB $. $( $j usage 'ralprg' avoids 'ax-10' 'ax-11' 'ax-12'; $) @@ -43775,7 +43785,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). ( vc cv wsbc wceq wi wral wa nfv eqeq2 imbi12d cpr wreu wrex wcel nfsbc1v vw wo sbceq1a dfsbcq reu8nf nfcv nfim nfralw eqeq1 imbi2d ralbidv anbi12d nfan rexprgf ralprg eqidd biantrur wb sbcieg adantl imbi1d bitr3id anbi2d - bitrd biantru adantr eqcom imbi2i anbi2i bitrdi orbi12d syl5bb ) ADEFUAZU + bitrd biantru adantr eqcom imbi2i anbi2i bitrdi orbi12d bitrid ) ADEFUAZU BAADKLZMZDLZVSNZOZKVRPZQZDVRUCZEGUDZFHUDZQZBCEFNZOZQZCBWJOZQZUGZAVTADUFLZ MDKUFVRADVSUEZADWPUEADWPUHADWPVSUIUJWIWFBVTEVSNZOZKVRPZQZCVTFVSNZOZKVRPZQ ZUGWOWEXAXEDEFGHBWTDBDRWSDKVRDVRUKZVTWRDWQWRDRULUMURCXDDCDRXCDKVRXFVTXBDW @@ -44511,7 +44521,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). 29-Jun-2011.) $) difsn $p |- ( -. A e. B -> ( B \ { A } ) = B ) $= ( vx wcel wn csn cdif cv wne wa eldifsn simpl nelelne ancld impbid2 eqrdv - syl5bb ) ABDEZCBAFGZBCHZSDTBDZTAIZJZRUATBAKRUCUAUAUBLRUAUBABTMNOQP $. + bitrid ) ABDEZCBAFGZBCHZSDTBDZTAIZJZRUATBAKRUCUAUAUBLRUAUBABTMNOQP $. $( Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) $) @@ -44921,7 +44931,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020.) $) preq2b $p |- ( ph -> ( { C , A } = { C , B } <-> A = B ) ) $= - ( cpr wceq prcom eqeq12i preq1b syl5bb ) DBIZDCIZJBDIZCDIZJABCJOQPRDBKDCK + ( cpr wceq prcom eqeq12i preq1b bitrid ) DBIZDCIZJBDIZCDIZJABCJOQPRDBKDCK LABCDEFGHMN $. $}