P. 46 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4501-4600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tpeq2d 4501	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3d 4502	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq123d 4503	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Theorem	tprot 4504	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Theorem	tpcoma 4505	Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
Theorem	tpcomb 4506	Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
Theorem	tpass 4507	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
Theorem	qdass 4508	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
Theorem	qdassr 4509	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
Theorem	tpidm12 4510	Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm13 4511	Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
Theorem	tpidm23 4512	Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm 4513	Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐴} = {𝐴}
Theorem	tppreq3 4514	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 4515	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 4516	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 4517	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 4518	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4516 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 ∈ {𝐴, 𝐵}
Theorem	ifpprsnss 4519	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 4520	A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 4521	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 4522	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
Theorem	tpid1 4523	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 4524	Closed theorem form of tpid1 4523. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷})
Theorem	tpid2 4525	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 4526	Closed theorem form of tpid2 4525. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷})
Theorem	tpid3g 4527	Closed theorem form of tpid3 4528. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	tpid3 4528	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 4529	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
Theorem	snnz 4530	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≠ ∅
Theorem	prnz 4531	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ≠ ∅
Theorem	prnzg 4532	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
Theorem	tpnz 4533	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅
Theorem	tpnzd 4534	A triplet containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ≠ ∅)
Theorem	raltpd 4535*	Convert a quantification over a triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜃))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	snssg 4536	The singleton of an element of a class is a subset of the class (general form of snss 4537). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
Theorem	snss 4537	The singleton of an element of a class is a subset of the class (inference form of snssg 4536). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)
Theorem	eldifsn 4538	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
Theorem	ssdifsn 4539	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	ssdifsnOLD 4540	Obsolete proof of ssdifsn 4539 as of 31-May-2022. (Contributed by Emmett Weisz, 7-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	elpwdifsn 4541	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 4542	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)
Theorem	neldifsn 4543	The class 𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Theorem	neldifsnd 4544	The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Theorem	rexdifsn 4545	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑))
Theorem	raldifsni 4546	Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ (∀𝑥 ∈ (𝐴 ∖ {𝐵}) ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 = 𝐵))
Theorem	raldifsnb 4547*	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 4548	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 4549	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 4550	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵}
Theorem	difprsn1 4551	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
Theorem	difprsn2 4552	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
Theorem	diftpsn3 4553	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 4554	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 4555	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 4556	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 4557	(𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 4549. (Contributed by David Moews, 1-May-2017.)
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵)
Theorem	difsnpss 4558	(𝐵 ∖ {𝐴}) is a proper subclass of 𝐵 if and only if 𝐴 is a member of 𝐵. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) ⊊ 𝐵)
Theorem	snssi 4559	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
Theorem	snssd 4560	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	difsnid 4561	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 4562	An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → 𝑌 ∈ (𝐵 ∖ {𝑋}))
Theorem	pw0 4563	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 4564	Compute the power set of the power set of the empty set. (See pw0 4563 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4652, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
⊢ 𝒫 {∅} = {∅, {∅}}
Theorem	snsspr1 4565	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
⊢ {𝐴} ⊆ {𝐴, 𝐵}
Theorem	snsspr2 4566	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
⊢ {𝐵} ⊆ {𝐴, 𝐵}
Theorem	snsstp1 4567	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp2 4568	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp3 4569	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prssg 4570	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 4571	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 4572	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prssd 4573	Deduction version of prssi 4572: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prsspwg 4574	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 4575	A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))))
Theorem	ssprsseq 4576	A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ⊆ {𝐶, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷}))
Theorem	sssn 4577	The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
Theorem	ssunsn2 4578	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 4655. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))
Theorem	ssunsn 4579	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶})) ↔ (𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})))
Theorem	eqsn 4580*	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	issn 4581*	A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧})
Theorem	n0snor2el 4582*	A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.)
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧}))
Theorem	ssunpr 4583	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷}))))
Theorem	sspr 4584	The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})))
Theorem	sstp 4585	The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))))
Theorem	tpss 4586	A triplet 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 4587	A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	sneqrg 4588	Closed form of sneqr 4589. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
Theorem	sneqr 4589	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 4590	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵)
Theorem	mosneq 4591*	There exists at most one set whose singleton is equal to a given class. See also moeq 3601. (Contributed by BJ, 24-Sep-2022.)
⊢ ∃*𝑥{𝑥} = 𝐴
Theorem	sneqbg 4592	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Theorem	snsspw 4593	The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.)
⊢ {𝐴} ⊆ 𝒫 𝐴
Theorem	prsspw 4594	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 4595	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 4596	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 4597	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 4598	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 4599	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
Theorem	prel12OLD 4600	Obsolete as of 16-Jun-2022. Use prel12g 4616 instead. (Contributed by NM, 17-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))