P. 38 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3701-3800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preq12 3701	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Theorem	preq1i 3702	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐶}
Theorem	preq2i 3703	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}
Theorem	preq12i 3704	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐷}
Theorem	preq1d 3705	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2d 3706	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12d 3707	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Theorem	tpeq1 3708	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2 3709	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3 3710	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq1d 3711	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2d 3712	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3d 3713	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq123d 3714	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Theorem	tprot 3715	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Theorem	tpcoma 3716	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
Theorem	tpcomb 3717	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
Theorem	tpass 3718	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
Theorem	qdass 3719	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
Theorem	qdassr 3720	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
Theorem	tpidm12 3721	Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm13 3722	Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
Theorem	tpidm23 3723	Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm 3724	Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐴} = {𝐴}
Theorem	tppreq3 3725	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 3726	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 3727	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 3728	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 3729	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 3730	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 3731	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 3732	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
Theorem	tpid1 3733	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 3734	Closed theorem form of tpid1 3733. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷})
Theorem	tpid2 3735	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 3736	Closed theorem form of tpid2 3735. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷})
Theorem	tpid3g 3737	Closed theorem form of tpid3 3738. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	tpid3 3738	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 3739	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
Theorem	snmg 3740*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴})
Theorem	snnz 3741	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≠ ∅
Theorem	snm 3742*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴}
Theorem	prmg 3743*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵})
Theorem	prnz 3744	A pair containing a set is not empty. It is also inhabited (see prm 3745). (Contributed by NM, 9-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ≠ ∅
Theorem	prm 3745*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴, 𝐵}
Theorem	prnzg 3746	A pair containing a set is not empty. It is also inhabited (see prmg 3743). (Contributed by FL, 19-Sep-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
Theorem	tpnz 3747	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅
Theorem	snssOLD 3748	Obsolete version of snss 3757 as of 1-Jan-2025. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)
Theorem	eldifsn 3749	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
Theorem	ssdifsn 3750	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	eldifsni 3751	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)
Theorem	neldifsn 3752	𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Theorem	neldifsnd 3753	𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Theorem	rexdifsn 3754	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑))
Theorem	snssb 3755	Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
Theorem	snssg 3756	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 3757	The singleton of an element of a class is a subset of the class (inference form of snssg 3756). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)
Theorem	snssgOLD 3758	Obsolete version of snssgOLD 3758 as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
Theorem	difsn 3759	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 3760	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵}
Theorem	difprsn1 3761	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
Theorem	difprsn2 3762	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
Theorem	diftpsn3 3763	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
Theorem	difpr 3764	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	difsnb 3765	(𝐵 ∖ {𝐴}) equals 𝐵 if and only if 𝐴 is not a member of 𝐵. Generalization of difsn 3759. (Contributed by David Moews, 1-May-2017.)
⊢ (¬ 𝐴 ∈ 𝐵 ↔ (𝐵 ∖ {𝐴}) = 𝐵)
Theorem	snssi 3766	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
Theorem	snssd 3767	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	difsnss 3768	If we remove a single element from a class then put it back in, we end up with a subset of the original class. If equality is decidable, we can replace subset with equality as seen in nndifsnid 6565. (Contributed by Jim Kingdon, 10-Aug-2018.)
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴)
Theorem	pw0 3769	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	snsspr1 3770	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
⊢ {𝐴} ⊆ {𝐴, 𝐵}
Theorem	snsspr2 3771	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
⊢ {𝐵} ⊆ {𝐴, 𝐵}
Theorem	snsstp1 3772	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp2 3773	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	snsstp3 3774	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prsstp12 3775	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ {𝐴, 𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prsstp13 3776	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ {𝐴, 𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prsstp23 3777	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ {𝐵, 𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Theorem	prss 3778	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prssg 3779	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	prssi 3780	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prssd 3781	Deduction version of prssi 3780: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶)
Theorem	prsspwg 3782	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	sssnr 3783	Empty set and the singleton itself are subsets of a singleton. Concerning the converse, see exmidsssn 4235. (Contributed by Jim Kingdon, 10-Aug-2018.)
⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
Theorem	sssnm 3784*	The inhabited subset of a singleton. (Contributed by Jim Kingdon, 10-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐴 ⊆ {𝐵} ↔ 𝐴 = {𝐵}))
Theorem	eqsnm 3785*	Two ways to express that an inhabited set equals a singleton. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))
Theorem	ssprr 3786	The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) → 𝐴 ⊆ {𝐵, 𝐶})
Theorem	sstpr 3787	The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ ((((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷})
Theorem	tpss 3788	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 3789	A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	sneqr 3790	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 3791	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵)
Theorem	sneqrg 3792	Closed form of sneqr 3790. (Contributed by Scott Fenton, 1-Apr-2011.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
Theorem	sneqbg 3793	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Theorem	snsspw 3794	The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
⊢ {𝐴} ⊆ 𝒫 𝐴
Theorem	prsspw 3795	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.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
Theorem	preqr1g 3796	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3798. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵))
Theorem	preqr2g 3797	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3799. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵))
Theorem	preqr1 3798	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 3799	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵)
Theorem	preq12b 3800	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))