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
Definition	df-tp 3501	Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
|- { A , B , C } = ( { A , B } u. { C } )
Definition	df-op 3502*	Definition of an ordered pair, equivalent to Kuratowski's definition { { A } , { A , B } } when the arguments are sets. Since the behavior of Kuratowski definition is not very useful for proper classes, we define it to be empty in this case (see opprc1 3693 and opprc2 3694). For Kuratowski's actual definition when the arguments are sets, see dfop 3670. Definition 9.1 of [Quine] p. 58 defines an ordered pair unconditionally as <. A , B >. = { { A } , { A , B } }, which has different behavior from our df-op 3502 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 3502 was chosen because it often makes proofs shorter by eliminating unnecessary sethood hypotheses. There are other ways to define ordered pairs. The basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition <. A , B >.2 = { { { A } , (/) } , { { B } } }. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition is <. A , B >.3 = { A , { A , B } }, but it requires the Axiom of Regularity for its justification and is not commonly used. Finally, an ordered pair of real numbers can be represented by a complex number. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
Definition	df-ot 3503	Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.)
|- <. A , B , C >. = <. <. A , B >. , C >.
Theorem	sneq 3504	Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> { A } = { B } )
Theorem	sneqi 3505	Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
|- A = B   =>    |- { A } = { B }
Theorem	sneqd 3506	Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> { A } = { B } )
Theorem	dfsn2 3507	Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
|- { A } = { A , A }
Theorem	elsng 3508	There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( A e. { B } <-> A = B ) )
Theorem	elsn 3509	There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
|- A e. _V   =>    |- ( A e. { B } <-> A = B )
Theorem	velsn 3510	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
|- ( x e. { A } <-> x = A )
Theorem	elsni 3511	There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
|- ( A e. { B } -> A = B )
Theorem	dfpr2 3512*	Alternate definition of unordered pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
|- { A , B } = { x | ( x = A \/ x = B ) }
Theorem	elprg 3513	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.)
|- ( A e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
Theorem	elpr 3514	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
|- A e. _V   =>    |- ( A e. { B , C } <-> ( A = B \/ A = C ) )
Theorem	elpr2 3515	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.)
|- B e. _V   &    |- C e. _V   =>    |- ( A e. { B , C } <-> ( A = B \/ A = C ) )
Theorem	elpri 3516	If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)
|- ( A e. { B , C } -> ( A = B \/ A = C ) )
Theorem	nelpri 3517	If an element doesn't match the items in an unordered pair, it is not in the unordered pair. (Contributed by David A. Wheeler, 10-May-2015.)
|- A =/= B   &    |- A =/= C   =>    |- -. A e. { B , C }
Theorem	prneli 3518	If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using e/. (Contributed by David A. Wheeler, 10-May-2015.)
|- A =/= B   &    |- A =/= C   =>    |- A e/ { B , C }
Theorem	nelprd 3519	If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( ph -> A =/= B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> -. A e. { B , C } )
Theorem	snidg 3520	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
|- ( A e. V -> A e. { A } )
Theorem	snidb 3521	A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.)
|- ( A e. _V <-> A e. { A } )
Theorem	snid 3522	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
|- A e. _V   =>    |- A e. { A }
Theorem	vsnid 3523	A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- x e. { x }
Theorem	elsn2g 3524	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set. (Contributed by NM, 28-Oct-2003.)
|- ( B e. V -> ( A e. { B } <-> A = B ) )
Theorem	elsn2 3525	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set. (Contributed by NM, 12-Jun-1994.)
|- B e. _V   =>    |- ( A e. { B } <-> A = B )
Theorem	mosn 3526*	A singleton has at most one element. This works whether A is a proper class or not, and in that sense can be seen as encompassing both snmg 3607 and snprc 3554. (Contributed by Jim Kingdon, 30-Aug-2018.)
|- E* x x e. { A }
Theorem	ralsnsg 3527*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
Theorem	ralsns 3528*	Substitution expressed in terms of quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
Theorem	rexsns 3529*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
|- ( E. x e. { A } ph <-> [. A / x ]. ph )
Theorem	ralsng 3530*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x e. { A } ph <-> ps ) )
Theorem	rexsng 3531*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( E. x e. { A } ph <-> ps ) )
Theorem	exsnrex 3532	There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( E. x M = { x } <-> E. x e. M M = { x } )
Theorem	ralsn 3533*	Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. { A } ph <-> ps )
Theorem	rexsn 3534*	Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E. x e. { A } ph <-> ps )
Theorem	eltpg 3535	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
|- ( A e. V -> ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) ) )
Theorem	eltpi 3536	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( A e. { B , C , D } -> ( A = B \/ A = C \/ A = D ) )
Theorem	eltp 3537	A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- A e. _V   =>    |- ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) )
Theorem	dftp2 3538*	Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)
|- { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }
Theorem	nfpr 3539	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x { A , B }
Theorem	ralprg 3540*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )
Theorem	rexprg 3541*	Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) )
Theorem	raltpg 3542*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) ) )
Theorem	rextpg 3543*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) ) )
Theorem	ralpr 3544*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( A. x e. { A , B } ph <-> ( ps /\ ch ) )
Theorem	rexpr 3545*	Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( E. x e. { A , B } ph <-> ( ps \/ ch ) )
Theorem	raltp 3546*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) )
Theorem	rextp 3547*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) )
Theorem	sbcsng 3548*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( [. A / x ]. ph <-> A. x e. { A } ph ) )
Theorem	nfsn 3549	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   =>    |- F/_ x { A }
Theorem	csbsng 3550	Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )
Theorem	disjsn 3551	Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
|- ( ( A i^i { B } ) = (/) <-> -. B e. A )
Theorem	disjsn2 3552	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
Theorem	disjpr2 3553	The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C , D } ) = (/) )
Theorem	snprc 3554	The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V <-> { A } = (/) )
Theorem	r19.12sn 3555*	Special case of r19.12 2512 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.)
|- ( A e. V -> ( E. x e. { A } A. y e. B ph <-> A. y e. B E. x e. { A } ph ) )
Theorem	rabsn 3556*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
|- ( B e. A -> { x e. A | x = B } = { B } )
Theorem	rabrsndc 3557*	A class abstraction over a decidable proposition restricted to a singleton is either the empty set or the singleton itself. (Contributed by Jim Kingdon, 8-Aug-2018.)
|- A e. _V   &    |- DECID ph   =>    |- ( M = { x e. { A } | ph } -> ( M = (/) \/ M = { A } ) )
Theorem	euabsn2 3558*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( E! x ph <-> E. y { x | ph } = { y } )
Theorem	euabsn 3559	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
|- ( E! x ph <-> E. x { x | ph } = { x } )
Theorem	reusn 3560*	A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|- ( E! x e. A ph <-> E. y { x e. A | ph } = { y } )
Theorem	absneu 3561	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )
Theorem	rabsneu 3562	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( ( A e. V /\ { x e. B | ph } = { A } ) -> E! x e. B ph )
Theorem	eusn 3563*	Two ways to express " A is a singleton." (Contributed by NM, 30-Oct-2010.)
|- ( E! x x e. A <-> E. x A = { x } )
Theorem	rabsnt 3564*	Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- B e. _V   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( { x e. A | ph } = { B } -> ps )
Theorem	prcom 3565	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- { A , B } = { B , A }
Theorem	preq1 3566	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
|- ( A = B -> { A , C } = { B , C } )
Theorem	preq2 3567	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> { C , A } = { C , B } )
Theorem	preq12 3568	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
Theorem	preq1i 3569	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { A , C } = { B , C }
Theorem	preq2i 3570	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { C , A } = { C , B }
Theorem	preq12i 3571	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &    |- C = D   =>    |- { A , C } = { B , D }
Theorem	preq1d 3572	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 3573	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 3574	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 3575	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 3576	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 3577	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 3578	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 3579	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 3580	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 3581	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   &    |- ( ph -> E = F )   =>    |- ( ph -> { A , C , E } = { B , D , F } )
Theorem	tprot 3582	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 3583	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 3584	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 3585	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- { A , B , C } = ( { A } u. { B , C } )
Theorem	qdass 3586	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A , B , C } u. { D } )
Theorem	qdassr 3587	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A } u. { B , C , D } )
Theorem	tpidm12 3588	Unordered triple { A , A , B } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , A , B } = { A , B }
Theorem	tpidm13 3589	Unordered triple { A , B , A } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , B , A } = { A , B }
Theorem	tpidm23 3590	Unordered triple { A , B , B } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , B , B } = { A , B }
Theorem	tpidm 3591	Unordered triple { A , A , A } is just an overlong way to write { A }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , A , A } = { A }
Theorem	tppreq3 3592	An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
|- ( B = C -> { A , B , C } = { A , B } )
Theorem	prid1g 3593	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( A e. V -> A e. { A , B } )
Theorem	prid2g 3594	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( B e. V -> B e. { A , B } )
Theorem	prid1 3595	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- A e. { A , B }
Theorem	prid2 3596	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- B e. _V   =>    |- B e. { A , B }
Theorem	prprc1 3597	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V -> { A , B } = { B } )
Theorem	prprc2 3598	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3599	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
|- ( ( -. A e. _V /\ -. B e. _V ) -> { A , B } = (/) )
Theorem	tpid1 3600	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   =>    |- A e. { A , B , C }