diff --git a/discouraged b/discouraged index 733979a51..3bb4a6212 100644 --- a/discouraged +++ b/discouraged @@ -18736,6 +18736,7 @@ New usage of "r19.30OLD" is discouraged (0 uses). New usage of "r19.35OLD" is discouraged (0 uses). New usage of "r1omALT" is discouraged (0 uses). New usage of "r1pwALT" is discouraged (0 uses). +New usage of "rabbiiaOLD" is discouraged (0 uses). New usage of "rabeqiOLD" is discouraged (0 uses). New usage of "rabid2OLD" is discouraged (0 uses). New usage of "rabrabiOLD" is discouraged (0 uses). @@ -21132,6 +21133,7 @@ Proof modification of "r19.30OLD" is discouraged (66 steps). Proof modification of "r19.35OLD" is discouraged (72 steps). Proof modification of "r1omALT" is discouraged (13 steps). Proof modification of "r1pwALT" is discouraged (151 steps). +Proof modification of "rabbiiaOLD" is discouraged (39 steps). Proof modification of "rabeqiOLD" is discouraged (59 steps). Proof modification of "rabid2OLD" is discouraged (57 steps). Proof modification of "rabrabiOLD" is discouraged (38 steps). diff --git a/set.mm b/set.mm index 9565b7c1d..983d4b40d 100644 --- a/set.mm +++ b/set.mm @@ -31590,107 +31590,39 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ~ df-ral . (Contributed by NM, 22-Nov-1994.) $) df-rab $a |- { x e. A | ph } = { x | ( x e. A /\ ph ) } $. - $( An "identity" law of concretion for restricted abstraction. Special case - of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.) $) - rabid $p |- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) ) $= - ( cv wcel wa crab df-rab abeq2i ) BDCEAFBABCGABCHI $. - - $( Abstract builder restricted to another restricted abstract builder. - (Contributed by Thierry Arnoux, 30-Aug-2017.) $) - rabrab $p |- { x e. { x e. A | ph } | ps } = { x e. A | ( ph /\ ps ) } $= - ( cv crab wcel wa cab rabid anbi1i anass bitri abbii df-rab 3eqtr4i ) CEZAC - DFZGZBHZCIQDGZABHZHZCIBCRFUBCDFTUCCTUAAHZBHUCSUDBACDJKUAABLMNBCROUBCDOP $. - - $( Membership in a restricted abstraction, implication. (Contributed by - Glauco Siliprandi, 26-Jun-2021.) $) - rabidim1 $p |- ( x e. { x e. A | ph } -> x e. A ) $= - ( cv crab wcel rabid simplbi ) BDZABCEFICFAABCGH $. - - ${ - rabid2f.1 $e |- F/_ x A $. - $( An "identity" law for restricted class abstraction. (Contributed by NM, - 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised - by Thierry Arnoux, 13-Mar-2017.) $) - rabid2f $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= - ( cv wcel wa cab wceq wi wal crab wral abeq2f pm4.71 bitr4i df-rab eqeq2i - wb albii df-ral 3bitr4i ) CBECFZAGZBHZIZUCAJZBKZCABCLZIABCMUFUCUDSZBKUHUD - BCDNUGUJBUCAOTPUIUECABCQRABCUAUB $. - $} - - ${ - $d x A $. - $( An "identity" law for restricted class abstraction. (Contributed by NM, - 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof - shortened by Wolf Lammen, 24-Nov-2024.) $) - rabid2 $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= - ( nfcv rabid2f ) ABCBCDE $. - - $( Obsolete version of ~ rabid2 as of 24-11-2024. (Contributed by NM, - 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) - (Proof modification is discouraged.) (New usage is discouraged.) $) - rabid2OLD $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= - ( cv wcel wa cab wceq wi wal crab abeq2 pm4.71 albii bitr4i df-rab eqeq2i - wral wb df-ral 3bitr4i ) CBDCEZAFZBGZHZUBAIZBJZCABCKZHABCRUEUBUCSZBJUGUCB - CLUFUIBUBAMNOUHUDCABCPQABCTUA $. - $} - - $( Equivalent wff's correspond to equal restricted class abstractions. - Closed theorem form of ~ rabbidva . (Contributed by NM, 25-Nov-2013.) $) - rabbi $p |- ( A. x e. A ( ps <-> ch ) - <-> { x e. A | ps } = { x e. A | ch } ) $= - ( cv wcel wa wb wal wceq wral crab abbi wi df-ral pm5.32 albii bitri df-rab - cab eqeq12i 3bitr4i ) CEDFZAGZUCBGZHZCIZUDCTZUECTZJABHZCDKZACDLZBCDLZJUDUEC - MUKUCUJNZCIUGUJCDOUNUFCUCABPQRULUHUMUIACDSBCDSUAUB $. - - $( The abstraction variable in a restricted class abstraction isn't free. - (Contributed by NM, 19-Mar-1997.) $) - nfrab1 $p |- F/_ x { x e. A | ph } $= - ( crab cv wcel wa cab df-rab nfab1 nfcxfr ) BABCDBECFAGZBHABCILBJK $. + $( *** Theorems using axioms up to ax-9 and ax-ext only: *** $) ${ - $d x y $. - nfrabw.1 $e |- F/ x ph $. - nfrabw.2 $e |- F/_ x A $. - $( A variable not free in a wff remains so in a restricted class - abstraction. Version of ~ nfrab with a disjoint variable condition, - which does not require ~ ax-13 . (Contributed by NM, 13-Oct-2003.) - Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) (Proof - shortened by Wolf Lammen, 23-Nov-2024.) $) - nfrabw $p |- F/_ x { y e. A | ph } $= - ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri nfan a1i nfabdw - mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCOUDBPNUCABBCDFQERSTUAUB $. - $( $j usage 'nfrabw' avoids 'ax-13'; $) - - $( Obsolete version of ~ nfrabw as of 23-Nov_2024. (Contributed by NM, - 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) - (New usage is discouraged.) (Proof modification is discouraged.) $) - nfrabwOLD $p |- F/_ x { y e. A | ph } $= - ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri a1i nfand nfabdw - mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCONUCABUCBPNBCDFQRABPNERSTUAU - B $. - $( $j usage 'nfrabwOLD' avoids 'ax-13'; $) + $d x ph $. + rabbidva2.1 $e |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) ) $. + $( Equivalent wff's yield equal restricted class abstractions. + (Contributed by Thierry Arnoux, 4-Feb-2017.) $) + rabbidva2 $p |- ( ph -> { x e. A | ps } = { x e. B | ch } ) $= + ( cv wcel wa cab crab abbidv df-rab 3eqtr4g ) ADHZEIBJZDKPFICJZDKBDELCDFL + AQRDGMBDENCDFNO $. $} ${ - $d x z $. $d y z $. $d z A $. - nfrab.1 $e |- F/ x ph $. - nfrab.2 $e |- F/_ x A $. - $( A variable not free in a wff remains so in a restricted class - abstraction. Usage of this theorem is discouraged because it depends on - ~ ax-13 . Use the weaker ~ nfrabw when possible. (Contributed by NM, - 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) - (New usage is discouraged.) $) - nfrab $p |- F/_ x { y e. A | ph } $= - ( vz crab cv wcel wa cab df-rab wnfc wtru nftru weq wal wn wnf eleq1w a1i - nfcri dvelimnf nfand adantl nfabd2 mptru nfcxfr ) BACDHCIDJZAKZCLZACDMBUL - NOUKBCCPBCQBRSZUKBTOUMUJABGIDJUJBCGBGDFUCGCDUAUDABTUMEUBUEUFUGUHUI $. + rabbia2.1 $e |- ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) $. + $( Equivalent wff's yield equal restricted class abstractions. + (Contributed by Glauco Siliprandi, 26-Jun-2021.) $) + rabbia2 $p |- { x e. A | ps } = { x e. B | ch } $= + ( crab wceq wtru cv wcel wa wb a1i rabbidva2 mptru ) ACDGBCEGHIABCDECJZDK + ALQEKBLMIFNOP $. $} ${ rabbiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $. $( Equivalent formulas yield equal restricted class abstractions (inference - form). (Contributed by NM, 22-May-1999.) $) + form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf + Lammen, 12-Jan-2025.) $) rabbiia $p |- { x e. A | ph } = { x e. A | ps } $= + ( cv wcel pm5.32i rabbia2 ) ABCDDCFDGABEHI $. + + $( Obsolete version of ~ rabbiia as of 12-Jan-2025. (Contributed by NM, + 22-May-1999.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + rabbiiaOLD $p |- { x e. A | ph } = { x e. A | ps } $= ( cv wcel wa cab crab pm5.32i abbii df-rab 3eqtr4i ) CFDGZAHZCIOBHZCIACDJ BCDJPQCOABEKLACDMBCDMN $. $} @@ -31704,45 +31636,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( wb cv wcel a1i rabbiia ) ABCDABFCGDHEIJ $. $} - ${ - rabbida.n $e |- F/ x ph $. - rabbida.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. - $( Equivalent wff's yield equal restricted class abstractions (deduction - form). Version of ~ rabbidva with disjoint variable condition replaced - by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) $) - rabbida $p |- ( ph -> { x e. A | ps } = { x e. A | ch } ) $= - ( wb wral crab wceq cv wcel ex ralrimi rabbi sylib ) ABCHZDEIBDEJCDEJKARD - EFADLEMRGNOBCDEPQ $. - $} - - ${ - rabbid.n $e |- F/ x ph $. - rabbid.1 $e |- ( ph -> ( ps <-> ch ) ) $. - $( Version of ~ rabbidv with disjoint variable condition replaced by - nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) $) - rabbid $p |- ( ph -> { x e. A | ps } = { x e. A | ch } ) $= - ( wb cv wcel adantr rabbida ) ABCDEFABCHDIEJGKL $. - $} - - ${ - $d x ph $. - rabbidva2.1 $e |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) ) $. - $( Equivalent wff's yield equal restricted class abstractions. - (Contributed by Thierry Arnoux, 4-Feb-2017.) $) - rabbidva2 $p |- ( ph -> { x e. A | ps } = { x e. B | ch } ) $= - ( cv wcel wa cab crab abbidv df-rab 3eqtr4g ) ADHZEIBJZDKPFICJZDKBDELCDFL - AQRDGMBDENCDFNO $. - $} - - ${ - rabbia2.1 $e |- ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) $. - $( Equivalent wff's yield equal restricted class abstractions. - (Contributed by Glauco Siliprandi, 26-Jun-2021.) $) - rabbia2 $p |- { x e. A | ps } = { x e. B | ch } $= - ( crab wceq wtru cv wcel wa wb a1i rabbidva2 mptru ) ACDGBCEGHIABCDECJZDK - ALQEKBLMIFNOP $. - $} - ${ $d x ph $. rabbidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. @@ -31763,15 +31656,32 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( wb cv wcel adantr rabbidva ) ABCDEABCGDHEIFJK $. $} + $( Swap with a membership relation in a restricted class abstraction. + (Contributed by NM, 4-Jul-2005.) $) + rabswap $p |- { x e. A | x e. B } = { x e. B | x e. A } $= + ( cv wcel ancom rabbia2 ) ADZCEZHBEZABCJIFG $. + ${ - rabeqf.1 $e |- F/_ x A $. - rabeqf.2 $e |- F/_ x B $. - $( Equality theorem for restricted class abstractions, with bound-variable - hypotheses instead of distinct variable restrictions. (Contributed by - NM, 7-Mar-2004.) $) - rabeqf $p |- ( A = B -> { x e. A | ph } = { x e. B | ph } ) $= - ( wceq cv wcel wa cab crab nfeq eleq2 anbi1d abbid df-rab 3eqtr4g ) CDGZB - HZCIZAJZBKTDIZAJZBKABCLABDLSUBUDBBCDEFMSUAUCACDTNOPABCQABDQR $. + $d x y A $. $d y ph $. $d x ps $. + cbvrabv.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Rule to change the bound variable in a restricted class abstraction, + using implicit substitution. (Contributed by NM, 26-May-1999.) Require + ` x ` , ` y ` be disjoint to avoid ~ ax-11 and ~ ax-13 . (Revised by + Steven Nguyen, 4-Dec-2022.) $) + cbvrabv $p |- { x e. A | ph } = { y e. A | ps } $= + ( cv wcel wa cab crab weq eleq1w anbi12d cbvabv df-rab 3eqtr4i ) CGEHZAIZ + CJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $} + + ${ + $d x A $. $d x ph $. + rabeqcda.1 $e |- ( ( ph /\ x e. A ) -> ps ) $. + $( When ` ps ` is always true in a context, a restricted class abstraction + is equal to the restricting class. Deduction form of ~ rabeqc . + (Contributed by Steven Nguyen, 7-Jun-2023.) $) + rabeqcda $p |- ( ph -> { x e. A | ps } = A ) $= + ( crab cv wcel wa cab df-rab ex pm4.71d bicomd abbi1dv eqtrid ) ABCDFCGDH + ZBIZCJDBCDKARCDAQRAQBAQBELMNOP $. $} ${ @@ -31783,15 +31693,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( cv wcel eleq2i anbi1i rabbia2 ) AABCDBFZCGKDGACDKEHIJ $. $( $j usage 'rabeqi' avoids 'ax-10' 'ax-11' 'ax-12'; $) - $( Obsolete version of ~ rabeqi as of 3-Jun-2024. (Contributed by Glauco - Siliprandi, 26-Jun-2021.) Avoid ~ ax-10 and ~ ax-11 . (Revised by Gino - Giotto, 20-Aug-2023.) (Proof modification is discouraged.) - (New usage is discouraged.) $) - rabeqiOLD $p |- { x e. A | ph } = { x e. B | ph } $= - ( wceq crab cv wcel wa cab nfth eleq2 anbi1d abbid df-rab 3eqtr4g ax-mp ) - CDFZABCGZABDGZFESBHZCIZAJZBKUBDIZAJZBKTUASUDUFBSBELSUCUEACDUBMNOABCPABDPQ - R $. - $( $j usage 'rabeqiOLD' avoids 'ax-10' 'ax-11'; $) $} ${ @@ -31830,6 +31731,46 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( crab rabbidva rabeqdv eqtrd ) ABDEICDEICDFIABCDEHJACDEFGKL $. $} + $( *** Theorems using axioms up to ax-9 , ax-10, ax-ext only: *** $) + + $( The abstraction variable in a restricted class abstraction isn't free. + (Contributed by NM, 19-Mar-1997.) $) + nfrab1 $p |- F/_ x { x e. A | ph } $= + ( crab cv wcel wa cab df-rab nfab1 nfcxfr ) BABCDBECFAGZBHABCILBJK $. + + $( *** Theorems using axioms up to ax-9 , ax-12, ax-ext only: *** $) + + $( An "identity" law of concretion for restricted abstraction. Special case + of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.) $) + rabid $p |- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) ) $= + ( cv wcel wa crab df-rab abeq2i ) BDCEAFBABCGABCHI $. + + $( Abstract builder restricted to another restricted abstract builder. + (Contributed by Thierry Arnoux, 30-Aug-2017.) $) + rabrab $p |- { x e. { x e. A | ph } | ps } = { x e. A | ( ph /\ ps ) } $= + ( cv crab wcel wa cab rabid anbi1i anass bitri abbii df-rab 3eqtr4i ) CEZAC + DFZGZBHZCIQDGZABHZHZCIBCRFUBCDFTUCCTUAAHZBHUCSUDBACDJKUAABLMNBCROUBCDOP $. + + ${ + $d x y $. $d A y $. $d ch y $. + rabrabi.1 $e |- ( x = y -> ( ch <-> ph ) ) $. + $( Abstract builder restricted to another restricted abstract builder with + implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid + ~ ax-10 , ~ ax-11 and ~ ax-12 . (Revised by Gino Giotto, + 12-Oct-2024.) $) + rabrabi $p |- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) } $= + ( wa crab cv wcel cab df-rab eleq2i wsb df-clab weq eleq1w wb bitri anass + bicomd equcoms anbi12d sbievw anbi1i rabbia2 ) BCBHZDAEFIZFDJZUIKZBHUJFKZ + CHZBHULUHHUKUMBUKUJEJFKZAHZELZKZUMUIUPUJAEFMNUQUOEDOUMUODEPUOUMEDEDQUNULA + CEDFRACSDEDEQCAGUBUCUDUETTUFULCBUATUG $. + $( $j usage 'rabrabi' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + + $( Membership in a restricted abstraction, implication. (Contributed by + Glauco Siliprandi, 26-Jun-2021.) $) + rabidim1 $p |- ( x e. { x e. A | ph } -> x e. A ) $= + ( cv crab wcel rabid simplbi ) BDZABCEFICFAABCGH $. + ${ rabeq2i.1 $e |- A = { x e. B | ph } $. $( Inference from equality of a class variable and a restricted class @@ -31838,10 +31779,88 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( cv wcel crab wa eleq2i rabid bitri ) BFZCGMABDHZGMDGAICNMEJABDKL $. $} - $( Swap with a membership relation in a restricted class abstraction. - (Contributed by NM, 4-Jul-2005.) $) - rabswap $p |- { x e. A | x e. B } = { x e. B | x e. A } $= - ( cv wcel ancom rabbia2 ) ADZCEZHBEZABCJIFG $. + ${ + $d A x y $. $d ph x $. $d ch y $. + rabrabiOLD.1 $e |- ( x = y -> ( ch <-> ph ) ) $. + $( Obsolete version of ~ rabrabi as of 12-Oct-2024. (Contributed by AV, + 2-Aug-2022.) Avoid ~ ax-10 and ~ ax-11 . (Revised by Gino Giotto, + 20-Aug-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + rabrabiOLD $p |- + { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) } $= + ( crab wa cbvrabv rabeqi rabrab eqtr3i ) BDCDFHZHBDAEFHZHCBIDFHBDNOCADEFG + JKCBDFLM $. + $( $j usage 'rabrabiOLD' avoids 'ax-10' 'ax-11'; $) + $} + + $( *** Theorems using axioms up to ax-12, ax-ext only: *** $) + + $( Equivalent wff's correspond to equal restricted class abstractions. + Closed theorem form of ~ rabbidva . (Contributed by NM, 25-Nov-2013.) $) + rabbi $p |- ( A. x e. A ( ps <-> ch ) + <-> { x e. A | ps } = { x e. A | ch } ) $= + ( cv wcel wa wb wal wceq wral crab abbi wi df-ral pm5.32 albii bitri df-rab + cab eqeq12i 3bitr4i ) CEDFZAGZUCBGZHZCIZUDCTZUECTZJABHZCDKZACDLZBCDLZJUDUEC + MUKUCUJNZCIUGUJCDOUNUFCUCABPQRULUHUMUIACDSBCDSUAUB $. + + ${ + rabbida.n $e |- F/ x ph $. + rabbida.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. + $( Equivalent wff's yield equal restricted class abstractions (deduction + form). Version of ~ rabbidva with disjoint variable condition replaced + by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) $) + rabbida $p |- ( ph -> { x e. A | ps } = { x e. A | ch } ) $= + ( wb wral crab wceq cv wcel ex ralrimi rabbi sylib ) ABCHZDEIBDEJCDEJKARD + EFADLEMRGNOBCDEPQ $. + $} + + ${ + rabbid.n $e |- F/ x ph $. + rabbid.1 $e |- ( ph -> ( ps <-> ch ) ) $. + $( Version of ~ rabbidv with disjoint variable condition replaced by + nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) $) + rabbid $p |- ( ph -> { x e. A | ps } = { x e. A | ch } ) $= + ( wb cv wcel adantr rabbida ) ABCDEFABCHDIEJGKL $. + $} + + ${ + rabid2f.1 $e |- F/_ x A $. + $( An "identity" law for restricted class abstraction. (Contributed by NM, + 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised + by Thierry Arnoux, 13-Mar-2017.) $) + rabid2f $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= + ( cv wcel wa cab wceq wi wal crab wral abeq2f pm4.71 bitr4i df-rab eqeq2i + wb albii df-ral 3bitr4i ) CBECFZAGZBHZIZUCAJZBKZCABCLZIABCMUFUCUDSZBKUHUD + BCDNUGUJBUCAOTPUIUECABCQRABCUAUB $. + $} + + ${ + $d x A $. + $( An "identity" law for restricted class abstraction. (Contributed by NM, + 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof + shortened by Wolf Lammen, 24-Nov-2024.) $) + rabid2 $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= + ( nfcv rabid2f ) ABCBCDE $. + + $( Obsolete version of ~ rabid2 as of 24-11-2024. (Contributed by NM, + 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + rabid2OLD $p |- ( A = { x e. A | ph } <-> A. x e. A ph ) $= + ( cv wcel wa cab wceq wi wal crab abeq2 pm4.71 albii bitr4i df-rab eqeq2i + wral wb df-ral 3bitr4i ) CBDCEZAFZBGZHZUBAIZBJZCABCKZHABCRUEUBUCSZBJUGUCB + CLUFUIBUBAMNOUHUDCABCPQABCTUA $. + $} + + ${ + rabeqf.1 $e |- F/_ x A $. + rabeqf.2 $e |- F/_ x B $. + $( Equality theorem for restricted class abstractions, with bound-variable + hypotheses instead of distinct variable restrictions. (Contributed by + NM, 7-Mar-2004.) $) + rabeqf $p |- ( A = B -> { x e. A | ph } = { x e. B | ph } ) $= + ( wceq cv wcel wa cab crab nfeq eleq2 anbi1d abbid df-rab 3eqtr4g ) CDGZB + HZCIZAJZBKTDIZAJZBKABCLABDLSUBUDBBCDEFMSUAUCACDTNOPABCQABDQR $. + $} ${ $d x y z $. $d A z $. $d ph z $. $d ps z $. @@ -31864,6 +31883,60 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( $j usage 'cbvrabw' avoids 'ax-13'; $) $} + ${ + $d x y $. + nfrabw.1 $e |- F/ x ph $. + nfrabw.2 $e |- F/_ x A $. + $( A variable not free in a wff remains so in a restricted class + abstraction. Version of ~ nfrab with a disjoint variable condition, + which does not require ~ ax-13 . (Contributed by NM, 13-Oct-2003.) + Avoid ~ ax-13 . (Revised by Gino Giotto, 10-Jan-2024.) (Proof + shortened by Wolf Lammen, 23-Nov-2024.) $) + nfrabw $p |- F/_ x { y e. A | ph } $= + ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri nfan a1i nfabdw + mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCOUDBPNUCABBCDFQERSTUAUB $. + $( $j usage 'nfrabw' avoids 'ax-13'; $) + + $( Obsolete version of ~ nfrabw as of 23-Nov_2024. (Contributed by NM, + 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + nfrabwOLD $p |- F/_ x { y e. A | ph } $= + ( crab cv wcel wa cab df-rab wnfc wtru nftru wnf nfcri a1i nfand nfabdw + mptru nfcxfr ) BACDGCHDIZAJZCKZACDLBUEMNUDBCCONUCABUCBPNBCDFQRABPNERSTUAU + B $. + $( $j usage 'nfrabwOLD' avoids 'ax-13'; $) + $} + + ${ + rabeqiOLD.1 $e |- A = B $. + $( Obsolete version of ~ rabeqi as of 3-Jun-2024. (Contributed by Glauco + Siliprandi, 26-Jun-2021.) Avoid ~ ax-10 and ~ ax-11 . (Revised by Gino + Giotto, 20-Aug-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + rabeqiOLD $p |- { x e. A | ph } = { x e. B | ph } $= + ( wceq crab cv wcel wa cab nfth eleq2 anbi1d abbid df-rab 3eqtr4g ax-mp ) + CDFZABCGZABDGZFESBHZCIZAJZBKUBDIZAJZBKTUASUDUFBSBELSUCUEACDUBMNOABCPABDPQ + R $. + $( $j usage 'rabeqiOLD' avoids 'ax-10' 'ax-11'; $) + $} + + $( *** Theorems using axioms ax-13 or axc11r: *** $) + + ${ + $d x z $. $d y z $. $d z A $. + nfrab.1 $e |- F/ x ph $. + nfrab.2 $e |- F/_ x A $. + $( A variable not free in a wff remains so in a restricted class + abstraction. Usage of this theorem is discouraged because it depends on + ~ ax-13 . Use the weaker ~ nfrabw when possible. (Contributed by NM, + 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) + (New usage is discouraged.) $) + nfrab $p |- F/_ x { y e. A | ph } $= + ( vz crab cv wcel wa cab df-rab wnfc wtru nftru weq wal wn wnf eleq1w a1i + nfcri dvelimnf nfand adantl nfabd2 mptru nfcxfr ) BACDHCIDJZAKZCLZACDMBUL + NOUKBCCPBCQBRSZUKBTOUMUJABGIDJUJBCGBGDFUCGCDUAUDABTUMEUBUEUFUGUHUI $. + $} + ${ $d x z $. $d y z $. $d A z $. $d ph z $. $d ps z $. cbvrab.1 $e |- F/_ x A $. @@ -31885,58 +31958,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is JUIUJUFUGUKACEULBDEULUM $. $} - ${ - $d x y A $. $d y ph $. $d x ps $. - cbvrabv.1 $e |- ( x = y -> ( ph <-> ps ) ) $. - $( Rule to change the bound variable in a restricted class abstraction, - using implicit substitution. (Contributed by NM, 26-May-1999.) Require - ` x ` , ` y ` be disjoint to avoid ~ ax-11 and ~ ax-13 . (Revised by - Steven Nguyen, 4-Dec-2022.) $) - cbvrabv $p |- { x e. A | ph } = { y e. A | ps } $= - ( cv wcel wa cab crab weq eleq1w anbi12d cbvabv df-rab 3eqtr4i ) CGEHZAIZ - CJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. - $} - - ${ - $d x y $. $d A y $. $d ch y $. - rabrabi.1 $e |- ( x = y -> ( ch <-> ph ) ) $. - $( Abstract builder restricted to another restricted abstract builder with - implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid - ~ ax-10 , ~ ax-11 and ~ ax-12 . (Revised by Gino Giotto, - 12-Oct-2024.) $) - rabrabi $p |- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) } $= - ( wa crab cv wcel cab df-rab eleq2i wsb df-clab weq eleq1w wb bitri anass - bicomd equcoms anbi12d sbievw anbi1i rabbia2 ) BCBHZDAEFIZFDJZUIKZBHUJFKZ - CHZBHULUHHUKUMBUKUJEJFKZAHZELZKZUMUIUPUJAEFMNUQUOEDOUMUODEPUOUMEDEDQUNULA - CEDFRACSDEDEQCAGUBUCUDUETTUFULCBUATUG $. - $( $j usage 'rabrabi' avoids 'ax-10' 'ax-11' 'ax-12'; $) - $} - - ${ - $d A x y $. $d ph x $. $d ch y $. - rabrabiOLD.1 $e |- ( x = y -> ( ch <-> ph ) ) $. - $( Obsolete version of ~ rabrabi as of 12-Oct-2024. (Contributed by AV, - 2-Aug-2022.) Avoid ~ ax-10 and ~ ax-11 . (Revised by Gino Giotto, - 20-Aug-2023.) (Proof modification is discouraged.) - (New usage is discouraged.) $) - rabrabiOLD $p |- - { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) } $= - ( crab wa cbvrabv rabeqi rabrab eqtr3i ) BDCDFHZHBDAEFHZHCBIDFHBDNOCADEFG - JKCBDFLM $. - $( $j usage 'rabrabiOLD' avoids 'ax-10' 'ax-11'; $) - $} - - ${ - $d x A $. $d x ph $. - rabeqcda.1 $e |- ( ( ph /\ x e. A ) -> ps ) $. - $( When ` ps ` is always true in a context, a restricted class abstraction - is equal to the restricting class. Deduction form of ~ rabeqc . - (Contributed by Steven Nguyen, 7-Jun-2023.) $) - rabeqcda $p |- ( ph -> { x e. A | ps } = A ) $= - ( crab cv wcel wa cab df-rab ex pm4.71d bicomd abbi1dv eqtrid ) ABCDFCGDH - ZBIZCJDBCDKARCDAQRAQBAQBELMNOP $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=