P. 41 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-tp 4001	Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
|- { A , B , C } = ( { A , B } u. { C } )
Syntax	cop 4002	Extend class notation to include ordered pair.
class <. A , B >.
Definition	df-op 4003*	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 4207, opprc2 4208, and 0nelop 4707). For Kuratowski's actual definition when the arguments are sets, see dfop 4183. For the justifying theorem (for sets) see opth 4692. See dfopif 4181 for an equivalent formulation using the if operation. 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 4003 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4003 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 } } }, justified by opthwiener 4719. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition <. A , B >._3 = { A , { A , B } } is justified by opthreg 8126, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is <. A , B >._4 = ( ( A X. { (/) } ) u. ( B X. { { (/) } } ) ), justified by opthprc 4898. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 12456. An ordered pair of real numbers can also be represented by a complex number as shown by cru 10602. Kuratowski's ordered pair definition is standard for ZFC set theory, but it is very inconvenient to use in New Foundations theory because it is not type-level; a common alternative definition in New Foundations is the Definition from [Rosser] p. 281. Since there are other ways to define ordered pairs, we discourage direct use of this definition so that most theorems won't depend on this particular construction; theorems will instead rely on dfopif 4181. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
Syntax	cotp 4004	Extend class notation to include ordered triple.
class <. A , B , C >.
Definition	df-ot 4005	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 4006	Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
|- ( A = B -> { A } = { B } )
Theorem	sneqi 4007	Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
|- A = B   =>    |- { A } = { B }
Theorem	sneqd 4008	Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
|- ( ph -> A = B )   =>    |- ( ph -> { A } = { B } )
Theorem	dfsn2 4009	Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
|- { A } = { A , A }
Theorem	elsn 4010*	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	dfpr2 4011*	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 4012	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	elpri 4013	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	elpr 4014	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 4015	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	nelpri 4016	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	nelprd 4017	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	eldifpr 4018	Membership in a set with two elements removed. Similar to eldifsn 4122 and eldiftp 4040. (Contributed by Mario Carneiro, 18-Jul-2017.)
|- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )
Theorem	elsncg 4019	There is only 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	elsnc 4020	There is only 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	elsni 4021	There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
|- ( A e. { B } -> A = B )
Theorem	snidg 4022	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 4023	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 4024	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	ssnid 4025	A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- x e. { x }
Theorem	elsnc2g 4026	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	elsnc2 4027	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	ralsnsg 4028*	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	rexsns 4029*	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	rexsnsOLD 4030*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) Obsolete as of 22-Aug-2018. Deletion blocked by r19.12snOLD 4063. Use rexsns 4029 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( E. x e. { A } ph <-> [. A / x ]. ph ) )
Theorem	ralsng 4031*	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 4032*	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	2ralsng 4033*	Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A } A. y e. { B } ph <-> ch ) )
Theorem	exsnrex 4034	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 4035*	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 4036*	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	elpwunsn 4037	Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.)
|- ( A e. ( ~P ( B u. { C } ) \ ~P B ) -> C e. A )
Theorem	eqoreldif 4038	An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020.)
|- ( B e. C -> ( A e. C <-> ( A = B \/ A e. ( C \ { B } ) ) ) )
Theorem	eltpg 4039	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	eldiftp 4040	Membership in a set with three elements removed. Similar to eldifsn 4122 and eldifpr 4018. (Contributed by David A. Wheeler, 22-Jul-2017.)
|- ( A e. ( B \ { C , D , E } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D /\ A =/= E ) ) )
Theorem	eltpi 4041	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 4042	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 4043*	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 4044	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x { A , B }
Theorem	ifpr 4045	Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.)
|- ( ( A e. C /\ B e. D ) -> if ( ph , A , B ) e. { A , B } )
Theorem	ralprg 4046*	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 4047*	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 4048*	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 4049*	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 4050*	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 4051*	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 4052*	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 4053*	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	nfsn 4054	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   =>    |- F/_ x { A }
Theorem	csbsng 4055	Distribute proper substitution through the singleton of a class. csbsng 4055 is derived from the virtual deduction proof csbsngVD 37151. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )
Theorem	csbprg 4056	Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
|- ( C e. V -> [_ C / x ]_ { A , B } = { [_ C / x ]_ A , [_ C / x ]_ B } )
Theorem	disjsn 4057	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 4058	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
Theorem	disjpr2 4059	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 4060	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, 21-Jun-1993.)
|- ( -. A e. _V <-> { A } = (/) )
Theorem	snnzb 4061	A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.)
|- ( A e. _V <-> { A } =/= (/) )
Theorem	r19.12sn 4062*	Special case of r19.12 2954 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 18-Mar-2020.)
|- ( A e. V -> ( E. x e. { A } A. y e. B ph <-> A. y e. B E. x e. { A } ph ) )
Theorem	r19.12snOLD 4063*	Older form of r19.12sn 4062. Obsolete as of 18-Mar-2020. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   =>    |- ( E. x e. { A } A. y e. B ph <-> A. y e. B E. x e. { A } ph )
Theorem	rabsn 4064*	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	rabsnifsb 4065*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.)
|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )
Theorem	rabsnif 4066*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- { x e. { A } | ph } = if ( ps , { A } , (/) )
Theorem	rabrsn 4067*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Proof shortened by AV, 21-Jul-2019.)
|- ( M = { x e. { A } | ph } -> ( M = (/) \/ M = { A } ) )
Theorem	euabsn2 4068*	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 4069	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 4070*	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 4071	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )
Theorem	rabsneu 4072	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 4073*	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 4074*	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 4075	Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
|- { A , B } = { B , A }
Theorem	preq1 4076	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
|- ( A = B -> { A , C } = { B , C } )
Theorem	preq2 4077	Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)
|- ( A = B -> { C , A } = { C , B } )
Theorem	preq12 4078	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
Theorem	preq1i 4079	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { A , C } = { B , C }
Theorem	preq2i 4080	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { C , A } = { C , B }
Theorem	preq12i 4081	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &    |- C = D   =>    |- { A , C } = { B , D }
Theorem	preq1d 4082	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 4083	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 4084	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 4085	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 4086	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 4087	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 4088	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 4089	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 4090	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 4091	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 4092	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 4093	Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 4094	Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 4095	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 4096	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 4097	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 4098	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 4099	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 4100	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 }