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	ralsng 3601*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	rexsng 3602*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	exsnrex 3603	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 3604*	Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	rexsn 3605*	Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	eltpg 3606	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
Theorem	eldiftp 3607	Membership in a set with three elements removed. Similar to eldifsn 3688 and eldifpr 3588. (Contributed by David A. Wheeler, 22-Jul-2017.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸)))
Theorem	eltpi 3608	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
Theorem	eltp 3609	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 3610*	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 3611	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥{𝐴, 𝐵}
Theorem	ralprg 3612*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	rexprg 3613*	Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)))
Theorem	raltpg 3614*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)))
Theorem	rextpg 3615*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)))
Theorem	ralpr 3616*	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 3617*	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 3618*	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 3619*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))
Theorem	sbcsng 3620*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝐴}𝜑))
Theorem	nfsn 3621	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝐴}
Theorem	csbsng 3622	Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})
Theorem	disjsn 3623	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 3624	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Theorem	disjpr2 3625	The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)
Theorem	snprc 3626	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 3627*	Special case of r19.12 2563 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 3628*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵})
Theorem	rabrsndc 3629*	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 3630*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	euabsn 3631	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥})
Theorem	reusn 3632*	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 3633	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑)
Theorem	rabsneu 3634	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑)
Theorem	eusn 3635*	Two ways to express "𝐴 is a singleton." (Contributed by NM, 30-Oct-2010.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	rabsnt 3636*	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 3637	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ {𝐴, 𝐵} = {𝐵, 𝐴}
Theorem	preq1 3638	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2 3639	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12 3640	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Theorem	preq1i 3641	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐶}
Theorem	preq2i 3642	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}
Theorem	preq12i 3643	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐷}
Theorem	preq1d 3644	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2d 3645	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12d 3646	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Theorem	tpeq1 3647	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2 3648	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3 3649	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq1d 3650	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2d 3651	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3d 3652	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq123d 3653	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Theorem	tprot 3654	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Theorem	tpcoma 3655	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
Theorem	tpcomb 3656	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
Theorem	tpass 3657	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
Theorem	qdass 3658	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
Theorem	qdassr 3659	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
Theorem	tpidm12 3660	Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm13 3661	Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
Theorem	tpidm23 3662	Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm 3663	Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐴} = {𝐴}
Theorem	tppreq3 3664	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 3665	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 3666	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 3667	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 3668	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 3669	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 3670	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 3671	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)
Theorem	tpid1 3672	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 3673	Closed theorem form of tpid1 3672. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐴, 𝐶, 𝐷})
Theorem	tpid2 3674	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 3675	Closed theorem form of tpid2 3674. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐴, 𝐷})
Theorem	tpid3g 3676	Closed theorem form of tpid3 3677. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	tpid3 3677	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 3678	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)
Theorem	snmg 3679*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴})
Theorem	snnz 3680	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ≠ ∅
Theorem	snm 3681*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴}
Theorem	prmg 3682*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴, 𝐵})
Theorem	prnz 3683	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ≠ ∅
Theorem	prm 3684*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 ∈ {𝐴, 𝐵}
Theorem	prnzg 3685	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)
Theorem	tpnz 3686	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴, 𝐵, 𝐶} ≠ ∅
Theorem	snss 3687	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)
Theorem	eldifsn 3688	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
Theorem	ssdifsn 3689	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
⊢ (𝐴 ⊆ (𝐵 ∖ {𝐶}) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐴))
Theorem	eldifsni 3690	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)
Theorem	neldifsn 3691	𝐴 is not in (𝐵 ∖ {𝐴}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
Theorem	neldifsnd 3692	𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Theorem	rexdifsn 3693	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝜑))
Theorem	snssg 3694	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
Theorem	difsn 3695	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 3696	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ({𝐴, 𝐵} ∖ {𝐴}) ⊆ {𝐵}
Theorem	difprsn1 3697	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
Theorem	difprsn2 3698	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
Theorem	diftpsn3 3699	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
Theorem	difpr 3700	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.)
⊢ (𝐴 ∖ {𝐵, 𝐶}) = ((𝐴 ∖ {𝐵}) ∖ {𝐶})