P. 36 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3501-3600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	disjdif2 3501	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
|- ( ( A i^i B ) = (/) -> ( A \ B ) = A )
Theorem	difun2 3502	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
|- ( ( A u. B ) \ B ) = ( A \ B )
Theorem	undifss 3503	Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A C_ B <-> ( A u. ( B \ A ) ) C_ B )
Theorem	ssdifin0 3504	A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
|- ( A C_ ( B \ C ) -> ( A i^i C ) = (/) )
Theorem	ssdifeq0 3505	A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.)
|- ( A C_ ( B \ A ) <-> A = (/) )
Theorem	ssundifim 3506	A consequence of inclusion in the union of two classes. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A C_ ( B u. C ) -> ( A \ B ) C_ C )
Theorem	difdifdirss 3507	Distributive law for class difference. In classical logic, as in Exercise 4.8 of [Stoll] p. 16, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A \ B ) \ C ) C_ ( ( A \ C ) \ ( B \ C ) )
Theorem	uneqdifeqim 3508	Two ways that A and B can "partition" C (when A and B don't overlap and A is a part of C). In classical logic, the second implication would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
Theorem	r19.2m 3509*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1638). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.)
|- ( ( E. y y e. A /\ A. x e. A ph ) -> E. x e. A ph )
Theorem	r19.2mOLD 3510*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1638). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) Obsolete version of r19.2m 3509 as of 7-Apr-2023. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E. x x e. A /\ A. x e. A ph ) -> E. x e. A ph )
Theorem	r19.3rm 3511*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.)
|- F/ x ph   =>    |- ( E. y y e. A -> ( ph <-> A. x e. A ph ) )
Theorem	r19.28m 3512*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- F/ x ph   =>    |- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( ph /\ A. x e. A ps ) ) )
Theorem	r19.3rmv 3513*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( E. y y e. A -> ( ph <-> A. x e. A ph ) )
Theorem	r19.9rmv 3514*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- ( E. y y e. A -> ( ph <-> E. x e. A ph ) )
Theorem	r19.28mv 3515*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( ph /\ A. x e. A ps ) ) )
Theorem	r19.45mv 3516*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
|- ( E. x x e. A -> ( E. x e. A ( ph \/ ps ) <-> ( ph \/ E. x e. A ps ) ) )
Theorem	r19.44mv 3517*	Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
|- ( E. y y e. A -> ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ ps ) ) )
Theorem	r19.27m 3518*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- F/ x ps   =>    |- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ ps ) ) )
Theorem	r19.27mv 3519*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ ps ) ) )
Theorem	rzal 3520*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A = (/) -> A. x e. A ph )
Theorem	rexn0 3521*	Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3522). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- ( E. x e. A ph -> A =/= (/) )
Theorem	rexm 3522*	Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.)
|- ( E. x e. A ph -> E. x x e. A )
Theorem	ralidm 3523*	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.)
|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )
Theorem	ral0 3524	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
|- A. x e. (/) ph
Theorem	rgenm 3525*	Generalization rule that eliminates an inhabited class requirement. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- ( ( E. x x e. A /\ x e. A ) -> ph )   =>    |- A. x e. A ph
Theorem	ralf0 3526*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.)
|- -. ph   =>    |- ( A. x e. A ph <-> A = (/) )
Theorem	ralm 3527	Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( ( E. x x e. A -> A. x e. A ph ) <-> A. x e. A ph )
Theorem	raaanlem 3528*	Special case of raaan 3529 where A is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x x e. A -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
Theorem	raaan 3529*	Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )
Theorem	raaanv 3530*	Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
|- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )
Theorem	sbss 3531*	Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|- ( [ y / x ] x C_ A <-> y C_ A )
Theorem	sbcssg 3532	Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) )
Theorem	dcun 3533	The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.)
|- ( ph -> DECID k e. A )   &    |- ( ph -> DECID k e. B )   =>    |- ( ph -> DECID k e. ( A u. B ) )
2.1.15  Conditional operator
Syntax	cif 3534	Extend class notation to include the conditional operator. See df-if 3535 for a description. (In older databases this was denoted "ded".)
class if ( ph , A , B )
Definition	df-if 3535*	Define the conditional operator. Read if ( ph , A , B ) as "if ph then A else B". See iftrue 3539 and iffalse 3542 for its values. In mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise." In the absence of excluded middle, this will tend to be useful where ph is decidable (in the sense of df-dc 835). (Contributed by NM, 15-May-1999.)
|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
Theorem	dfif6 3536*	An alternate definition of the conditional operator df-if 3535 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } )
Theorem	ifeq1 3537	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A = B -> if ( ph , A , C ) = if ( ph , B , C ) )
Theorem	ifeq2 3538	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A = B -> if ( ph , C , A ) = if ( ph , C , B ) )
Theorem	iftrue 3539	Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> if ( ph , A , B ) = A )
Theorem	iftruei 3540	Inference associated with iftrue 3539. (Contributed by BJ, 7-Oct-2018.)
|- ph   =>    |- if ( ph , A , B ) = A
Theorem	iftrued 3541	Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ch )   =>    |- ( ph -> if ( ch , A , B ) = A )
Theorem	iffalse 3542	Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
|- ( -. ph -> if ( ph , A , B ) = B )
Theorem	iffalsei 3543	Inference associated with iffalse 3542. (Contributed by BJ, 7-Oct-2018.)
|- -. ph   =>    |- if ( ph , A , B ) = B
Theorem	iffalsed 3544	Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> -. ch )   =>    |- ( ph -> if ( ch , A , B ) = B )
Theorem	ifnefalse 3545	When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs versus applying iffalse 3542 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( A =/= B -> if ( A = B , C , D ) = D )
Theorem	ifsbdc 3546	Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.)
|- ( if ( ph , A , B ) = A -> C = D )   &    |- ( if ( ph , A , B ) = B -> C = E )   =>    |- (DECID ph -> C = if ( ph , D , E ) )
Theorem	dfif3 3547*	Alternate definition of the conditional operator df-if 3535. Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- C = { x | ph }   =>    |- if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) )
Theorem	ifssun 3548	A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , B ) C_ ( A u. B )
Theorem	ifidss 3549	A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , A ) C_ A
Theorem	ifeq12 3550	Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.)
|- ( ( A = B /\ C = D ) -> if ( ph , A , C ) = if ( ph , B , D ) )
Theorem	ifeq1d 3551	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> if ( ps , A , C ) = if ( ps , B , C ) )
Theorem	ifeq2d 3552	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> if ( ps , C , A ) = if ( ps , C , B ) )
Theorem	ifeq12d 3553	Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> if ( ps , A , C ) = if ( ps , B , D ) )
Theorem	ifbi 3554	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ( ( ph <-> ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )
Theorem	ifbid 3555	Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> if ( ps , A , B ) = if ( ch , A , B ) )
Theorem	ifbieq1d 3556	Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> A = B )   =>    |- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )
Theorem	ifbieq2i 3557	Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph <-> ps )   &    |- A = B   =>    |- if ( ph , C , A ) = if ( ps , C , B )
Theorem	ifbieq2d 3558	Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> A = B )   =>    |- ( ph -> if ( ps , C , A ) = if ( ch , C , B ) )
Theorem	ifbieq12i 3559	Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.)
|- ( ph <-> ps )   &    |- A = C   &    |- B = D   =>    |- if ( ph , A , B ) = if ( ps , C , D )
Theorem	ifbieq12d 3560	Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )
Theorem	nfifd 3561	Deduction version of nfif 3562. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x if ( ps , A , B ) )
Theorem	nfif 3562	Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   =>    |- F/_ x if ( ph , A , B )
Theorem	ifcldadc 3563	Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.)
|- ( ( ph /\ ps ) -> A e. C )   &    |- ( ( ph /\ -. ps ) -> B e. C )   &    |- ( ph -> DECID ps )   =>    |- ( ph -> if ( ps , A , B ) e. C )
Theorem	ifeq1dadc 3564	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( ph /\ ps ) -> A = B )   &    |- ( ph -> DECID ps )   =>    |- ( ph -> if ( ps , A , C ) = if ( ps , B , C ) )
Theorem	ifeq2dadc 3565	Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( ph /\ -. ps ) -> A = B )   &    |- ( ph -> DECID ps )   =>    |- ( ph -> if ( ps , C , A ) = if ( ps , C , B ) )
Theorem	ifbothdadc 3566	A formula th containing a decidable conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 3-Jun-2022.)
|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )   &    |- ( B = if ( ph , A , B ) -> ( ch <-> th ) )   &    |- ( ( et /\ ph ) -> ps )   &    |- ( ( et /\ -. ph ) -> ch )   &    |- ( et -> DECID ph )   =>    |- ( et -> th )
Theorem	ifbothdc 3567	A wff th containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.)
|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )   &    |- ( B = if ( ph , A , B ) -> ( ch <-> th ) )   =>    |- ( ( ps /\ ch /\ DECID ph ) -> th )
Theorem	ifiddc 3568	Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
|- (DECID ph -> if ( ph , A , A ) = A )
Theorem	eqifdc 3569	Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.)
|- (DECID ph -> ( A = if ( ph , B , C ) <-> ( ( ph /\ A = B ) \/ ( -. ph /\ A = C ) ) ) )
Theorem	ifcldcd 3570	Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   &    |- ( ph -> DECID ps )   =>    |- ( ph -> if ( ps , A , B ) e. C )
Theorem	ifnotdc 3571	Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.)
|- (DECID ph -> if ( -. ph , A , B ) = if ( ph , B , A ) )
Theorem	ifandc 3572	Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- (DECID ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
Theorem	ifordc 3573	Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- (DECID ph -> if ( ( ph \/ ps ) , A , B ) = if ( ph , A , if ( ps , A , B ) ) )
Theorem	ifmdc 3574	If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.)
|- ( A e. if ( ph , B , C ) -> DECID ph )
2.1.16  Power classes
Syntax	cpw 3575	Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.)
class ~P A
Theorem	pwjust 3576*	Soundness justification theorem for df-pw 3577. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- { x | x C_ A } = { y | y C_ A }
Definition	df-pw 3577*	Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of _V. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if A is { 3 , 5 , 7 }, then ~P A is { (/) , { 3 } , { 5 } , { 7 } , { 3 , 5 } , { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } }. We will later introduce the Axiom of Power Sets. Still later we will prove that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 5-Aug-1993.)
|- ~P A = { x | x C_ A }
Theorem	pweq 3578	Equality theorem for power class. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> ~P A = ~P B )
Theorem	pweqi 3579	Equality inference for power class. (Contributed by NM, 27-Nov-2013.)
|- A = B   =>    |- ~P A = ~P B
Theorem	pweqd 3580	Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> ~P A = ~P B )
Theorem	elpw 3581	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.)
|- A e. _V   =>    |- ( A e. ~P B <-> A C_ B )
Theorem	velpw 3582*	Setvar variable membership in a power class (common case). See elpw 3581. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( x e. ~P A <-> x C_ A )
Theorem	elpwg 3583	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 6-Aug-2000.)
|- ( A e. V -> ( A e. ~P B <-> A C_ B ) )
Theorem	elpwi 3584	Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
|- ( A e. ~P B -> A C_ B )
Theorem	elpwb 3585	Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.)
|- ( A e. ~P B <-> ( A e. _V /\ A C_ B ) )
Theorem	elpwid 3586	An element of a power class is a subclass. Deduction form of elpwi 3584. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. ~P B )   =>    |- ( ph -> A C_ B )
Theorem	elelpwi 3587	If A belongs to a part of C then A belongs to C. (Contributed by FL, 3-Aug-2009.)
|- ( ( A e. B /\ B e. ~P C ) -> A e. C )
Theorem	nfpw 3588	Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
|- F/_ x A   =>    |- F/_ x ~P A
Theorem	pwidg 3589	Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( A e. V -> A e. ~P A )
Theorem	pwid 3590	A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- A e. ~P A
Theorem	pwss 3591*	Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.)
|- ( ~P A C_ B <-> A. x ( x C_ A -> x e. B ) )
2.1.17  Unordered and ordered pairs
Syntax	csn 3592	Extend class notation to include singleton.
class { A }
Syntax	cpr 3593	Extend class notation to include unordered pair.
class { A , B }
Syntax	ctp 3594	Extend class notation to include unordered triplet.
class { A , B , C }
Syntax	cop 3595	Extend class notation to include ordered pair.
class <. A , B >.
Syntax	cotp 3596	Extend class notation to include ordered triple.
class <. A , B , C >.
Theorem	snjust 3597*	Soundness justification theorem for df-sn 3598. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- { x | x = A } = { y | y = A }
Definition	df-sn 3598*	Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of _V, although it is not very meaningful in this case. For an alternate definition see dfsn2 3606. (Contributed by NM, 5-Aug-1993.)
|- { A } = { x | x = A }
Definition	df-pr 3599	Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. They are unordered, so { A , B } = { B , A } as proven by prcom 3668. For a more traditional definition, but requiring a dummy variable, see dfpr2 3611. (Contributed by NM, 5-Aug-1993.)
|- { A , B } = ( { A } u. { B } )
Definition	df-tp 3600	Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
|- { A , B , C } = ( { A , B } u. { C } )