diff --git a/set.mm b/set.mm index 22ebbcad59..43d6402452 100644 --- a/set.mm +++ b/set.mm @@ -30923,16 +30923,39 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $. $} + ${ + $d x z $. $d y z $. $d z A $. $d z ps $. $d z ph $. + cbvralf.1 $e |- F/_ x A $. + cbvralf.2 $e |- F/_ y A $. + cbvralf.3 $e |- F/ y ph $. + cbvralf.4 $e |- F/ x ps $. + cbvralf.5 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Rule used to change bound variables, using implicit substitution. Usage + of this theorem is discouraged because it depends on ~ ax-13 . Use the + weaker ~ cbvralfw when possible. (Contributed by NM, 7-Mar-2004.) + (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) $) + cbvralf $p |- ( A. x e. A ph <-> A. y e. A ps ) $= + ( vz cv wcel wi wal wral wsb nfv nfcri nfim nfs1v sbequ12 imbi12d cbvalv1 + weq eleq1w nfsb sbequ sbie bitrdi bitri df-ral 3bitr4i ) CLEMZANZCOZDLEMZ + BNZDOZACEPBDEPUPKLEMZACKQZNZKOUSUOVBCKUOKRUTVACCKEFSACKUATCKUEUNUTAVACKEU + FACKUBUCUDVBURKDUTVADDKEGSACKDHUGTURKRKDUEZUTUQVABKDEUFVCVAACDQBAKDCUHABC + DIJUIUJUCUDUKACEULBDEULUM $. + + $( Rule used to change bound variables, using implicit substitution. Usage + of this theorem is discouraged because it depends on ~ ax-13 . Use the + weaker ~ cbvrexfw when possible. (Contributed by FL, 27-Apr-2008.) + (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) $) + cbvrexf $p |- ( E. x e. A ph <-> E. y e. A ps ) $= + ( wn wral wrex nfn weq notbid cbvralf notbii dfrex2 3bitr4i ) AKZCELZKBKZ + DELZKACEMBDEMUBUDUAUCCDEFGADHNBCINCDOABJPQRACESBDEST $. + $} + $( Extend wff notation to include restricted existential uniqueness. $) wreu $a wff E! x e. A ph $. $( Extend wff notation to include restricted "at most one". $) wrmo $a wff E* x e. A ph $. - $( Extend class notation to include the restricted class abstraction (class - builder). $) - crab $a class { x e. A | ph } $. - $( Define restricted "at most one". Note: This notation is most often used to express that ` ph ` holds for @@ -30959,6 +30982,113 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is (Contributed by NM, 22-Nov-1994.) $) df-reu $a |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) ) $. + $( *** Theorems using axioms up to ax-4 only: *** $) + + $( Restricted uniqueness in terms of "at most one". (Contributed by NM, + 23-May-1999.) (Revised by NM, 16-Jun-2017.) $) + reu5 $p |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) ) $= + ( cv wcel wa weu wex wmo wreu wrex wrmo df-eu df-reu df-rex anbi12i 3bitr4i + df-rmo ) BDCEAFZBGSBHZSBIZFABCJABCKZABCLZFSBMABCNUBTUCUAABCOABCRPQ $. + + $( Restricted existential uniqueness implies restricted "at most one." + (Contributed by NM, 16-Jun-2017.) $) + reurmo $p |- ( E! x e. A ph -> E* x e. A ph ) $= + ( wreu wrex wrmo reu5 simprbi ) ABCDABCEABCFABCGH $. + + $( Restricted unique existence implies restricted existence. (Contributed by + NM, 19-Aug-1999.) $) + reurex $p |- ( E! x e. A ph -> E. x e. A ph ) $= + ( wreu wrex wrmo reu5 simplbi ) ABCDABCEABCFABCGH $. + + $( Unrestricted "at most one" implies restricted "at most one". (Contributed + by NM, 16-Jun-2017.) $) + mormo $p |- ( E* x ph -> E* x e. A ph ) $= + ( wmo cv wcel wa wrmo moan df-rmo sylibr ) ABDBECFZAGBDABCHALBIABCJK $. + + $( Cancellation law for restricted at-most-one quantification. (Contributed + by Peter Mazsa, 24-May-2018.) $) + rmoanid $p |- ( E* x e. A ( x e. A /\ ph ) <-> E* x e. A ph ) $= + ( cv wcel wa wmo wrmo anabs5 mobii df-rmo 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC + HONBMAIJNBCKABCKL $. + + $( Cancellation law for restricted unique existential quantification. + (Contributed by Peter Mazsa, 12-Feb-2018.) $) + reuanid $p |- ( E! x e. A ( x e. A /\ ph ) <-> E! x e. A ph ) $= + ( cv wcel wa weu wreu anabs5 eubii df-reu 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC + HONBMAIJNBCKABCKL $. + + ${ + rmobiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $. + $( Formula-building rule for restricted existential quantifier (inference + form). (Contributed by NM, 16-Jun-2017.) $) + rmobiia $p |- ( E* x e. A ph <-> E* x e. A ps ) $= + ( cv wcel wa wmo wrmo pm5.32i mobii df-rmo 3bitr4i ) CFDGZAHZCIOBHZCIACDJ + BCDJPQCOABEKLACDMBCDMN $. + + $( Formula-building rule for restricted existential quantifier (inference + form). (Contributed by NM, 14-Nov-2004.) $) + reubiia $p |- ( E! x e. A ph <-> E! x e. A ps ) $= + ( cv wcel wa weu wreu pm5.32i eubii df-reu 3bitr4i ) CFDGZAHZCIOBHZCIACDJ + BCDJPQCOABEKLACDMBCDMN $. + $} + + ${ + rmobii.1 $e |- ( ph <-> ps ) $. + $( Formula-building rule for restricted existential quantifier (inference + form). (Contributed by NM, 16-Jun-2017.) $) + rmobii $p |- ( E* x e. A ph <-> E* x e. A ps ) $= + ( wb cv wcel a1i rmobiia ) ABCDABFCGDHEIJ $. + + $( Formula-building rule for restricted existential quantifier (inference + form). (Contributed by NM, 22-Oct-1999.) $) + reubii $p |- ( E! x e. A ph <-> E! x e. A ps ) $= + ( wb cv wcel a1i reubiia ) ABCDABFCGDHEIJ $. + $} + + $( Double restricted existential uniqueness, analogous to ~ 2eu2ex . + (Contributed by Alexander van der Vekens, 25-Jun-2017.) $) + 2reu2rex $p |- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph ) $= + ( wreu wrex reurex reximi syl ) ACEFZBDFKBDGACEGZBDGKBDHKLBDACEHIJ $. + + $( *** Theorems using axioms up to ax-5 only: *** $) + + ${ + $d x ph $. + rmobidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. + $( Formula-building rule for restricted existential quantifier (deduction + form). (Contributed by NM, 16-Jun-2017.) Avoid ~ ax-6 , ~ ax-7 , + ~ ax-12 . (Revised by Wolf Lammen, 23-Nov-2024.) $) + rmobidva $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $= + ( cv wcel wa wmo wrmo pm5.32da mobidv df-rmo 3bitr4g ) ADGEHZBIZDJPCIZDJB + DEKCDEKAQRDAPBCFLMBDENCDENO $. + $( $j usage 'rmobidva' avoids 'ax-6' 'ax-7' 'ax-12'; $) + + $( Formula-building rule for restricted existential quantifier (deduction + form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised + by Wolf Lammen, 14-Jan-2023.) $) + reubidva $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $= + ( cv wcel wa weu wreu pm5.32da eubidv df-reu 3bitr4g ) ADGEHZBIZDJPCIZDJB + DEKCDEKAQRDAPBCFLMBDENCDENO $. + $} + + ${ + $d x ph $. + rmobidv.1 $e |- ( ph -> ( ps <-> ch ) ) $. + $( Formula-building rule for restricted existential quantifier (deduction + form). (Contributed by NM, 16-Jun-2017.) $) + rmobidv $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $= + ( wb cv wcel adantr rmobidva ) ABCDEABCGDHEIFJK $. + + $( Formula-building rule for restricted existential quantifier (deduction + form). (Contributed by NM, 17-Oct-1996.) $) + reubidv $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $= + ( wb cv wcel adantr reubidva ) ABCDEABCGDHEIFJK $. + $} + + $( Extend class notation to include the restricted class abstraction (class + builder). $) + crab $a class { x e. A | ph } $. + $( Define a restricted class abstraction (class builder): ` { x e. A | ph } ` is the class of all sets ` x ` in ` A ` such that ` ph ( x ) ` is true. Definition of [TakeutiZaring] p. 20. @@ -30971,18 +31101,6 @@ 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 ) } $. - $( Cancellation law for restricted unique existential quantification. - (Contributed by Peter Mazsa, 12-Feb-2018.) $) - reuanid $p |- ( E! x e. A ( x e. A /\ ph ) <-> E! x e. A ph ) $= - ( cv wcel wa weu wreu anabs5 eubii df-reu 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC - HONBMAIJNBCKABCKL $. - - $( Cancellation law for restricted at-most-one quantification. (Contributed - by Peter Mazsa, 24-May-2018.) $) - rmoanid $p |- ( E* x e. A ( x e. A /\ ph ) <-> E* x e. A ph ) $= - ( cv wcel wa wmo wrmo anabs5 mobii df-rmo 3bitr4i ) BDCEZMAFZFZBGNBGNBCHABC - HONBMAIJNBCKABCKL $. - $( The setvar ` x ` is not free in ` E! x e. A ph ` . (Contributed by NM, 19-Mar-1997.) $) nfreu1 $p |- F/ x E! x e. A ph $= @@ -31185,43 +31303,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ELCDELARSDFAQBCGMNBDEOCDEOP $. $} - ${ - $d x ph $. - reubidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. - $( Formula-building rule for restricted existential quantifier (deduction - form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised - by Wolf Lammen, 14-Jan-2023.) $) - reubidva $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $= - ( cv wcel wa weu wreu pm5.32da eubidv df-reu 3bitr4g ) ADGEHZBIZDJPCIZDJB - DEKCDEKAQRDAPBCFLMBDENCDENO $. - $} - - ${ - $d x ph $. - reubidv.1 $e |- ( ph -> ( ps <-> ch ) ) $. - $( Formula-building rule for restricted existential quantifier (deduction - form). (Contributed by NM, 17-Oct-1996.) $) - reubidv $p |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) ) $= - ( wb cv wcel adantr reubidva ) ABCDEABCGDHEIFJK $. - $} - - ${ - reubiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $. - $( Formula-building rule for restricted existential quantifier (inference - form). (Contributed by NM, 14-Nov-2004.) $) - reubiia $p |- ( E! x e. A ph <-> E! x e. A ps ) $= - ( cv wcel wa weu wreu pm5.32i eubii df-reu 3bitr4i ) CFDGZAHZCIOBHZCIACDJ - BCDJPQCOABEKLACDMBCDMN $. - $} - - ${ - reubii.1 $e |- ( ph <-> ps ) $. - $( Formula-building rule for restricted existential quantifier (inference - form). (Contributed by NM, 22-Oct-1999.) $) - reubii $p |- ( E! x e. A ph <-> E! x e. A ps ) $= - ( wb cv wcel a1i reubiia ) ABCDABFCGDHEIJ $. - $} - ${ rmobida.1 $e |- F/ x ph $. rmobida.2 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. @@ -31234,15 +31315,7 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ${ $d x ph $. - rmobidva.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. - $( Formula-building rule for restricted existential quantifier (deduction - form). (Contributed by NM, 16-Jun-2017.) Avoid ~ ax-6 , ~ ax-7 , - ~ ax-12 . (Revised by Wolf Lammen, 23-Nov-2024.) $) - rmobidva $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $= - ( cv wcel wa wmo wrmo pm5.32da mobidv df-rmo 3bitr4g ) ADGEHZBIZDJPCIZDJB - DEKCDEKAQRDAPBCFLMBDENCDENO $. - $( $j usage 'rmobidva' avoids 'ax-6' 'ax-7' 'ax-12'; $) - + rmobidvaOLD.1 $e |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) ) $. $( Obsolete version of ~ rmobidv as of 23-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) $) @@ -31250,32 +31323,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( nfv rmobida ) ABCDEADGFH $. $} - ${ - $d x ph $. - rmobidv.1 $e |- ( ph -> ( ps <-> ch ) ) $. - $( Formula-building rule for restricted existential quantifier (deduction - form). (Contributed by NM, 16-Jun-2017.) $) - rmobidv $p |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) ) $= - ( wb cv wcel adantr rmobidva ) ABCDEABCGDHEIFJK $. - $} - - ${ - rmobiia.1 $e |- ( x e. A -> ( ph <-> ps ) ) $. - $( Formula-building rule for restricted existential quantifier (inference - form). (Contributed by NM, 16-Jun-2017.) $) - rmobiia $p |- ( E* x e. A ph <-> E* x e. A ps ) $= - ( cv wcel wa wmo wrmo pm5.32i mobii df-rmo 3bitr4i ) CFDGZAHZCIOBHZCIACDJ - BCDJPQCOABEKLACDMBCDMN $. - $} - - ${ - rmobii.1 $e |- ( ph <-> ps ) $. - $( Formula-building rule for restricted existential quantifier (inference - form). (Contributed by NM, 16-Jun-2017.) $) - rmobii $p |- ( E* x e. A ph <-> E* x e. A ps ) $= - ( wb cv wcel a1i rmobiia ) ABCDABFCGDHEIJ $. - $} - ${ reueq1f.1 $e |- F/_ x A $. reueq1f.2 $e |- F/_ x B $. @@ -31347,32 +31394,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is JUEGZAHUMUEACKULUNAUJUCUDQSTSUAUB $. $} - $( Unrestricted "at most one" implies restricted "at most one". (Contributed - by NM, 16-Jun-2017.) $) - mormo $p |- ( E* x ph -> E* x e. A ph ) $= - ( wmo cv wcel wa wrmo moan df-rmo sylibr ) ABDBECFZAGBDABCHALBIABCJK $. - - $( Restricted uniqueness in terms of "at most one". (Contributed by NM, - 23-May-1999.) (Revised by NM, 16-Jun-2017.) $) - reu5 $p |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) ) $= - ( cv wcel wa weu wex wmo wreu wrex wrmo df-eu df-reu df-rex anbi12i 3bitr4i - df-rmo ) BDCEAFZBGSBHZSBIZFABCJABCKZABCLZFSBMABCNUBTUCUAABCOABCRPQ $. - - $( Restricted unique existence implies restricted existence. (Contributed by - NM, 19-Aug-1999.) $) - reurex $p |- ( E! x e. A ph -> E. x e. A ph ) $= - ( wreu wrex wrmo reu5 simplbi ) ABCDABCEABCFABCGH $. - - $( Double restricted existential uniqueness, analogous to ~ 2eu2ex . - (Contributed by Alexander van der Vekens, 25-Jun-2017.) $) - 2reu2rex $p |- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph ) $= - ( wreu wrex reurex reximi syl ) ACEFZBDFKBDGACEGZBDGKBDHKLBDACEHIJ $. - - $( Restricted existential uniqueness implies restricted "at most one." - (Contributed by NM, 16-Jun-2017.) $) - reurmo $p |- ( E! x e. A ph -> E* x e. A ph ) $= - ( wreu wrex wrmo reu5 simprbi ) ABCDABCEABCFABCGH $. - $( Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) $) rmo5 $p |- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) ) $= @@ -31395,33 +31416,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is BCJBCDKABQCABPABPELMNO $. $} - ${ - $d x z $. $d y z $. $d z A $. $d z ps $. $d z ph $. - cbvralf.1 $e |- F/_ x A $. - cbvralf.2 $e |- F/_ y A $. - cbvralf.3 $e |- F/ y ph $. - cbvralf.4 $e |- F/ x ps $. - cbvralf.5 $e |- ( x = y -> ( ph <-> ps ) ) $. - $( Rule used to change bound variables, using implicit substitution. Usage - of this theorem is discouraged because it depends on ~ ax-13 . Use the - weaker ~ cbvralfw when possible. (Contributed by NM, 7-Mar-2004.) - (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) $) - cbvralf $p |- ( A. x e. A ph <-> A. y e. A ps ) $= - ( vz cv wcel wi wal wral wsb nfv nfcri nfim nfs1v sbequ12 imbi12d cbvalv1 - weq eleq1w nfsb sbequ sbie bitrdi bitri df-ral 3bitr4i ) CLEMZANZCOZDLEMZ - BNZDOZACEPBDEPUPKLEMZACKQZNZKOUSUOVBCKUOKRUTVACCKEFSACKUATCKUEUNUTAVACKEU - FACKUBUCUDVBURKDUTVADDKEGSACKDHUGTURKRKDUEZUTUQVABKDEUFVCVAACDQBAKDCUHABC - DIJUIUJUCUDUKACEULBDEULUM $. - - $( Rule used to change bound variables, using implicit substitution. Usage - of this theorem is discouraged because it depends on ~ ax-13 . Use the - weaker ~ cbvrexfw when possible. (Contributed by FL, 27-Apr-2008.) - (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) $) - cbvrexf $p |- ( E. x e. A ph <-> E. y e. A ps ) $= - ( wn wral wrex nfn weq notbid cbvralf notbii dfrex2 3bitr4i ) AKZCELZKBKZ - DELZKACEMBDEMUBUDUAUCCDEFGADHNBCINCDOABJPQRACESBDEST $. - $} - ${ $d x y A $. cbvrmow.1 $e |- F/ y ph $.