P. 48 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4701-4800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prid1 4701	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ {𝐴, 𝐵}
Theorem	prid2 4702	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4700 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 ∈ {𝐴, 𝐵}
Theorem	ifpprsnss 4703	An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021.)
⊢ (𝑃 = {𝐴, 𝐵} → if-(𝐴 = 𝐵, 𝑃 = {𝐴}, {𝐴, 𝐵} ⊆ 𝑃))
Theorem	prprc1 4704	A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 4705	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 4706	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
Theorem	tpid1 4707	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 4708	Closed theorem form of tpid1 4707. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷})
Theorem	tpid2 4709	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 4710	Closed theorem form of tpid2 4709. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷})
Theorem	tpid3g 4711	Closed theorem form of tpid3 4712. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	tpid3 4712	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.)
⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}
Theorem	snnzg 4713	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
Theorem	snn0d 4714	The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝐴} ≠ ∅)
Theorem	snnz 4715	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≠ ∅
Theorem	prnz 4716	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ≠ ∅
Theorem	prnzg 4717	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
Theorem	tpnz 4718	An unordered triple containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅
Theorem	tpnzd 4719	An unordered triple containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ≠ ∅)
Theorem	raltpd 4720*	Convert a universal quantification over an unordered triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	snssb 4721	Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
Theorem	snssg 4722	The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
Theorem	snss 4723	The singleton of an element of a class is a subset of the class (inference form of snssg 4722). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)
Theorem	snssi 4724	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
Theorem	snssd 4725	The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝐴} ⊆ 𝐵)
Theorem	eldifsn 4726	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
Theorem	eldifsnd 4727	Membership in a set with an element removed : deduction version. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ {𝐶}))
Theorem	ssdifsn 4728	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	elpwdifsn 4729	A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆) → 𝑆 ∈ 𝒫 (𝑉 ∖ {𝐴}))
Theorem	eldifsni 4730	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)
Theorem	eldifsnneq 4731	An element of a difference with a singleton is not equal to the element of that singleton. Note that (¬ 𝐴 ∈ {𝐶} → ¬ 𝐴 = 𝐶) need not hold if 𝐴 is a proper class. (Contributed by BJ, 18-Mar-2023.) (Proof shortened by Steven Nguyen, 1-Jun-2023.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → ¬ 𝐴 = 𝐶)
Theorem	neldifsn 4732	The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Theorem	neldifsnd 4733	The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Theorem	rexdifsn 4734	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑))
Theorem	raldifsni 4735	Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ (∀𝑥 ∈ (𝐴 ∖ {𝐵}) ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝐵))
Theorem	raldifsnb 4736	Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ≠ 𝑌 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ {𝑌})𝜑)
Theorem	eldifvsn 4737	A set is an element of the universal class excluding a singleton iff it is not the singleton element. (Contributed by AV, 7-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (V ∖ {𝐵}) ↔ 𝐴 ≠ 𝐵))
Theorem	difsn 4738	An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∖ {𝐴}) = 𝐵)
Theorem	difprsnss 4739	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵}
Theorem	difprsn1 4740	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
Theorem	difprsn2 4741	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
Theorem	diftpsn3 4742	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
Theorem	difpr 4743	Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018.)
⊢ (𝐴 ∖ {𝐵, 𝐶}) = ((𝐴 ∖ {𝐵}) ∖ {𝐶})
Theorem	tpprceq3 4744	An unordered triple is an unordered pair if one of its elements is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
⊢ (¬ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐵) → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵})
Theorem	tppreqb 4745	An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018.)
⊢ (¬ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵) ↔ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵})
Theorem	difsnb 4746	(𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 4738. (Contributed by David Moews, 1-May-2017.)
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵)
Theorem	difsnpss 4747	(𝐵 ∖ {𝐴}) is a proper subclass of 𝐵 if and only if 𝐴 is a member of 𝐵. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) ⊊ 𝐵)
Theorem	difsnid 4748	If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.)
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Theorem	eldifeldifsn 4749	An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑌 ∈ (𝐵 ∖ {𝑋}))
Theorem	pw0 4750	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝒫 ∅ = {∅}
Theorem	pwpw0 4751	Compute the power set of the power set of the empty set. (See pw0 4750 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4838, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
⊢ 𝒫 {∅} = {∅, {∅}}
Theorem	snsspr1 4752	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
⊢ {𝐴} ⊆ {𝐴, 𝐵}
Theorem	snsspr2 4753	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
⊢ {𝐵} ⊆ {𝐴, 𝐵}
Theorem	snsstp1 4754	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp2 4755	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp3 4756	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prssg 4757	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 22-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
Theorem	prss 4758	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prssi 4759	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prssd 4760	Deduction version of prssi 4759: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prsspwg 4761	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.) (Revised by NM, 18-Jan-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ssprss 4762	A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))))
Theorem	ssprsseq 4763	A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
Theorem	sssn 4764	The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
Theorem	ssunsn2 4765	The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 4840. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))
Theorem	ssunsn 4766	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶})) ↔ (𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})))
Theorem	eqsn 4767*	Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))
Theorem	eqsnd 4768*	Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023.) (Proof shortened by SN, 3-Jul-2025.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	eqsndOLD 4769*	Obsolete version of eqsnd 4768 as of 3-Jul-2025. (Contributed by Thierry Arnoux, 10-May-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	issn 4770*	A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧})
Theorem	n0snor2el 4771*	A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
Theorem	ssunpr 4772	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷}))))
Theorem	sspr 4773	The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})))
Theorem	sstp 4774	The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))))
Theorem	tpss 4775	An unordered triple of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	tpssi 4776	An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	sneqrg 4777	Closed form of sneqr 4778. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
Theorem	sneqr 4778	If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 27-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} = {𝐵} → 𝐴 = 𝐵)
Theorem	snsssn 4779	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵)
Theorem	mosneq 4780*	There exists at most one set whose singleton is equal to a given class. See also moeq 3655. (Contributed by BJ, 24-Sep-2022.)
⊢ ∃*𝑥{𝑥} = 𝐴
Theorem	sneqbg 4781	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Theorem	snsspw 4782	The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.)
⊢ {𝐴} ⊆ 𝒫 𝐴
Theorem	prsspw 4783	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
Theorem	preq1b 4784	Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ({𝐴, 𝐶} = {𝐵, 𝐶} ↔ 𝐴 = 𝐵))
Theorem	preq2b 4785	Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ({𝐶, 𝐴} = {𝐶, 𝐵} ↔ 𝐴 = 𝐵))
Theorem	preqr1 4786	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵)
Theorem	preqr2 4787	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵)
Theorem	preq12b 4788	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
Theorem	opthpr 4789	An unordered pair has the ordered pair property (compare opth 5423) under certain conditions. (Contributed by NM, 27-Mar-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	preqr1g 4790	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4786. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵))
Theorem	preq12bg 4791	Closed form of preq12b 4788. (Contributed by Scott Fenton, 28-Mar-2014.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
Theorem	prneimg 4792	Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Theorem	prneimg2 4793	Two pairs are not equal if their counterparts are not equal. (Contributed by AV, 5-Sep-2025.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} ↔ ((𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷) ∧ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐶))))
Theorem	prnebg 4794	A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Theorem	pr1eqbg 4795	A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))
Theorem	pr1nebg 4796	A (proper) pair is not equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 ≠ 𝐶 ↔ {𝐴, 𝐵} ≠ {𝐵, 𝐶}))
Theorem	preqsnd 4797	Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.) (Revised by AV, 13-Jun-2022.) (Revised by AV, 16-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
Theorem	prnesn 4798	A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≠ {𝐶})
Theorem	prneprprc 4799	A proper unordered pair is not an improper unordered pair. (Contributed by AV, 13-Jun-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ ¬ 𝐶 ∈ V) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})
Theorem	preqsn 4800	Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 12-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))