P. 37 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3601-3700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prneli 3601	If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using ∉. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐴 ∉ {𝐵, 𝐶}
Theorem	nelprd 3602	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.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})
Theorem	eldifpr 3603	Membership in a set with two elements removed. Similar to eldifsn 3703 and eldiftp 3622. (Contributed by Mario Carneiro, 18-Jul-2017.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))
Theorem	rexdifpr 3604	Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.)
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑))
Theorem	snidg 3605	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
Theorem	snidb 3606	A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.)
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
Theorem	snid 3607	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ {𝐴}
Theorem	vsnid 3608	A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 𝑥 ∈ {𝑥}
Theorem	elsn2g 3609	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	elsn2 3610	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Theorem	nelsn 3611	If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.)
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})
Theorem	mosn 3612*	A singleton has at most one element. This works whether 𝐴 is a proper class or not, and in that sense can be seen as encompassing both snmg 3694 and snprc 3641. (Contributed by Jim Kingdon, 30-Aug-2018.)
⊢ ∃*𝑥 𝑥 ∈ {𝐴}
Theorem	ralsnsg 3613*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑))
Theorem	ralsns 3614*	Substitution expressed in terms of quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑))
Theorem	rexsns 3615*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)
Theorem	ralsng 3616*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	rexsng 3617*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	exsnrex 3618	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.)
⊢ (∃𝑥 𝑀 = {𝑥} ↔ ∃𝑥 ∈ 𝑀 𝑀 = {𝑥})
Theorem	ralsn 3619*	Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	rexsn 3620*	Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	eltpg 3621	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
Theorem	eldiftp 3622	Membership in a set with three elements removed. Similar to eldifsn 3703 and eldifpr 3603. (Contributed by David A. Wheeler, 22-Jul-2017.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸)))
Theorem	eltpi 3623	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
Theorem	eltp 3624	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.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
Theorem	dftp2 3625*	Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)
⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)}
Theorem	nfpr 3626	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥{𝐴, 𝐵}
Theorem	ralprg 3627*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	rexprg 3628*	Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)))
Theorem	raltpg 3629*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)))
Theorem	rextpg 3630*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)))
Theorem	ralpr 3631*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	rexpr 3632*	Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))
Theorem	raltp 3633*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	rextp 3634*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))
Theorem	sbcsng 3635*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝐴}𝜑))
Theorem	nfsn 3636	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝐴}
Theorem	csbsng 3637	Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})
Theorem	disjsn 3638	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.)
⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)
Theorem	disjsn2 3639	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Theorem	disjpr2 3640	The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)
Theorem	snprc 3641	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.)
⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
Theorem	r19.12sn 3642*	Special case of r19.12 2572 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑))
Theorem	rabsn 3643*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵})
Theorem	rabrsndc 3644*	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.)
⊢ 𝐴 ∈ V    &   ⊢ DECID 𝜑    ⇒   ⊢ (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴}))
Theorem	euabsn2 3645*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	euabsn 3646	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥})
Theorem	reusn 3647*	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.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦{𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦})
Theorem	absneu 3648	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑)
Theorem	rabsneu 3649	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑)
Theorem	eusn 3650*	Two ways to express "𝐴 is a singleton". (Contributed by NM, 30-Oct-2010.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	rabsnt 3651*	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.)
⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝜓)
Theorem	prcom 3652	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ {𝐴, 𝐵} = {𝐵, 𝐴}
Theorem	preq1 3653	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2 3654	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12 3655	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Theorem	preq1i 3656	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐶}
Theorem	preq2i 3657	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}
Theorem	preq12i 3658	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐷}
Theorem	preq1d 3659	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2d 3660	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12d 3661	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Theorem	tpeq1 3662	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2 3663	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3 3664	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq1d 3665	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2d 3666	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3d 3667	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq123d 3668	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Theorem	tprot 3669	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Theorem	tpcoma 3670	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
Theorem	tpcomb 3671	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
Theorem	tpass 3672	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
Theorem	qdass 3673	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
Theorem	qdassr 3674	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
Theorem	tpidm12 3675	Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm13 3676	Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
Theorem	tpidm23 3677	Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm 3678	Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐴} = {𝐴}
Theorem	tppreq3 3679	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.)
⊢ (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵})
Theorem	prid1g 3680	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
Theorem	prid2g 3681	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})
Theorem	prid1 3682	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ {𝐴, 𝐵}
Theorem	prid2 3683	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 ∈ {𝐴, 𝐵}
Theorem	prprc1 3684	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 3685	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 3686	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
Theorem	tpid1 3687	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}
Theorem	tpid1g 3688	Closed theorem form of tpid1 3687. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷})
Theorem	tpid2 3689	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Theorem	tpid2g 3690	Closed theorem form of tpid2 3689. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷})
Theorem	tpid3g 3691	Closed theorem form of tpid3 3692. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	tpid3 3692	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}
Theorem	snnzg 3693	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
Theorem	snmg 3694*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴})
Theorem	snnz 3695	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≠ ∅
Theorem	snm 3696*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴}
Theorem	prmg 3697*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵})
Theorem	prnz 3698	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ≠ ∅
Theorem	prm 3699*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴, 𝐵}
Theorem	prnzg 3700	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)