P. 35 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3401-3500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexsnsOLD 3401*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) Obsolete as of 22-Aug-2018. Use rexsns 3400 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (A ∈ 𝑉 → (∃x ∈ {A}φ ↔ [A / x]φ))
Theorem	ralsng 3402*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ 𝑉 → (∀x ∈ {A}φ ↔ ψ))
Theorem	rexsng 3403*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ 𝑉 → (∃x ∈ {A}φ ↔ ψ))
Theorem	exsnrex 3404	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.)
⊢ (∃x 𝑀 = {x} ↔ ∃x ∈ 𝑀 𝑀 = {x})
Theorem	ralsn 3405*	Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ {A}φ ↔ ψ)
Theorem	rexsn 3406*	Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ {A}φ ↔ ψ)
Theorem	eltpg 3407	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
⊢ (A ∈ 𝑉 → (A ∈ {B, 𝐶, 𝐷} ↔ (A = B ∨ A = 𝐶 ∨ A = 𝐷)))
Theorem	eltpi 3408	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (A ∈ {B, 𝐶, 𝐷} → (A = B ∨ A = 𝐶 ∨ A = 𝐷))
Theorem	eltp 3409	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.)
⊢ A ∈ V    ⇒   ⊢ (A ∈ {B, 𝐶, 𝐷} ↔ (A = B ∨ A = 𝐶 ∨ A = 𝐷))
Theorem	dftp2 3410*	Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)
⊢ {A, B, 𝐶} = {x ∣ (x = A ∨ x = B ∨ x = 𝐶)}
Theorem	nfpr 3411	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx{A, B}
Theorem	ralprg 3412*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∀x ∈ {A, B}φ ↔ (ψ ∧ χ)))
Theorem	rexprg 3413*	Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∃x ∈ {A, B}φ ↔ (ψ ∨ χ)))
Theorem	raltpg 3414*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    &   ⊢ (x = 𝐶 → (φ ↔ θ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀x ∈ {A, B, 𝐶}φ ↔ (ψ ∧ χ ∧ θ)))
Theorem	rextpg 3415*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    &   ⊢ (x = 𝐶 → (φ ↔ θ))    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃x ∈ {A, B, 𝐶}φ ↔ (ψ ∨ χ ∨ θ)))
Theorem	ralpr 3416*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    ⇒   ⊢ (∀x ∈ {A, B}φ ↔ (ψ ∧ χ))
Theorem	rexpr 3417*	Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    ⇒   ⊢ (∃x ∈ {A, B}φ ↔ (ψ ∨ χ))
Theorem	raltp 3418*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    &   ⊢ (x = 𝐶 → (φ ↔ θ))    ⇒   ⊢ (∀x ∈ {A, B, 𝐶}φ ↔ (ψ ∧ χ ∧ θ))
Theorem	rextp 3419*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    &   ⊢ (x = 𝐶 → (φ ↔ θ))    ⇒   ⊢ (∃x ∈ {A, B, 𝐶}φ ↔ (ψ ∨ χ ∨ θ))
Theorem	sbcsng 3420*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (A ∈ 𝑉 → ([A / x]φ ↔ ∀x ∈ {A}φ))
Theorem	nfsn 3421	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
⊢ ℲxA    ⇒   ⊢ Ⅎx{A}
Theorem	csbsng 3422	Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ 𝑉 → ⦋A / x⦌{B} = {⦋A / x⦌B})
Theorem	disjsn 3423	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.)
⊢ ((A ∩ {B}) = ∅ ↔ ¬ B ∈ A)
Theorem	disjsn2 3424	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
⊢ (A ≠ B → ({A} ∩ {B}) = ∅)
Theorem	disjpr2 3425	The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
⊢ (((A ≠ 𝐶 ∧ B ≠ 𝐶) ∧ (A ≠ 𝐷 ∧ B ≠ 𝐷)) → ({A, B} ∩ {𝐶, 𝐷}) = ∅)
Theorem	snprc 3426	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.)
⊢ (¬ A ∈ V ↔ {A} = ∅)
Theorem	r19.12sn 3427*	Special case of r19.12 2416 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ A ∈ V    ⇒   ⊢ (∃x ∈ {A}∀y ∈ B φ ↔ ∀y ∈ B ∃x ∈ {A}φ)
Theorem	rabsn 3428*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
⊢ (B ∈ A → {x ∈ A ∣ x = B} = {B})
Theorem	rabrsndc 3429*	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.)
⊢ A ∈ V    &   ⊢ DECID φ    ⇒   ⊢ (𝑀 = {x ∈ {A} ∣ φ} → (𝑀 = ∅ ∨ 𝑀 = {A}))
Theorem	euabsn2 3430*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∃!xφ ↔ ∃y{x ∣ φ} = {y})
Theorem	euabsn 3431	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
⊢ (∃!xφ ↔ ∃x{x ∣ φ} = {x})
Theorem	reusn 3432*	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.)
⊢ (∃!x ∈ A φ ↔ ∃y{x ∈ A ∣ φ} = {y})
Theorem	absneu 3433	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
⊢ ((A ∈ 𝑉 ∧ {x ∣ φ} = {A}) → ∃!xφ)
Theorem	rabsneu 3434	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ ((A ∈ 𝑉 ∧ {x ∈ B ∣ φ} = {A}) → ∃!x ∈ B φ)
Theorem	eusn 3435*	Two ways to express "A is a singleton." (Contributed by NM, 30-Oct-2010.)
⊢ (∃!x x ∈ A ↔ ∃x A = {x})
Theorem	rabsnt 3436*	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.)
⊢ B ∈ V    &   ⊢ (x = B → (φ ↔ ψ))    ⇒   ⊢ ({x ∈ A ∣ φ} = {B} → ψ)
Theorem	prcom 3437	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ {A, B} = {B, A}
Theorem	preq1 3438	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
⊢ (A = B → {A, 𝐶} = {B, 𝐶})
Theorem	preq2 3439	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
⊢ (A = B → {𝐶, A} = {𝐶, B})
Theorem	preq12 3440	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ ((A = 𝐶 ∧ B = 𝐷) → {A, B} = {𝐶, 𝐷})
Theorem	preq1i 3441	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ A = B    ⇒   ⊢ {A, 𝐶} = {B, 𝐶}
Theorem	preq2i 3442	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ A = B    ⇒   ⊢ {𝐶, A} = {𝐶, B}
Theorem	preq12i 3443	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ {A, 𝐶} = {B, 𝐷}
Theorem	preq1d 3444	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {A, 𝐶} = {B, 𝐶})
Theorem	preq2d 3445	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {𝐶, A} = {𝐶, B})
Theorem	preq12d 3446	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → {A, 𝐶} = {B, 𝐷})
Theorem	tpeq1 3447	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (A = B → {A, 𝐶, 𝐷} = {B, 𝐶, 𝐷})
Theorem	tpeq2 3448	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (A = B → {𝐶, A, 𝐷} = {𝐶, B, 𝐷})
Theorem	tpeq3 3449	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (A = B → {𝐶, 𝐷, A} = {𝐶, 𝐷, B})
Theorem	tpeq1d 3450	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {A, 𝐶, 𝐷} = {B, 𝐶, 𝐷})
Theorem	tpeq2d 3451	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {𝐶, A, 𝐷} = {𝐶, B, 𝐷})
Theorem	tpeq3d 3452	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {𝐶, 𝐷, A} = {𝐶, 𝐷, B})
Theorem	tpeq123d 3453	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    &   ⊢ (φ → 𝐸 = 𝐹)    ⇒   ⊢ (φ → {A, 𝐶, 𝐸} = {B, 𝐷, 𝐹})
Theorem	tprot 3454	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {A, B, 𝐶} = {B, 𝐶, A}
Theorem	tpcoma 3455	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {A, B, 𝐶} = {B, A, 𝐶}
Theorem	tpcomb 3456	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
⊢ {A, B, 𝐶} = {A, 𝐶, B}
Theorem	tpass 3457	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {A, B, 𝐶} = ({A} ∪ {B, 𝐶})
Theorem	qdass 3458	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({A, B} ∪ {𝐶, 𝐷}) = ({A, B, 𝐶} ∪ {𝐷})
Theorem	qdassr 3459	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({A, B} ∪ {𝐶, 𝐷}) = ({A} ∪ {B, 𝐶, 𝐷})
Theorem	tpidm12 3460	Unordered triple {A, A, B} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {A, A, B} = {A, B}
Theorem	tpidm13 3461	Unordered triple {A, B, A} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {A, B, A} = {A, B}
Theorem	tpidm23 3462	Unordered triple {A, B, B} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {A, B, B} = {A, B}
Theorem	tpidm 3463	Unordered triple {A, A, A} is just an overlong way to write {A}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {A, A, A} = {A}
Theorem	tppreq3 3464	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.)
⊢ (B = 𝐶 → {A, B, 𝐶} = {A, B})
Theorem	prid1g 3465	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (A ∈ 𝑉 → A ∈ {A, B})
Theorem	prid2g 3466	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (B ∈ 𝑉 → B ∈ {A, B})
Theorem	prid1 3467	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ A ∈ V    ⇒   ⊢ A ∈ {A, B}
Theorem	prid2 3468	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
⊢ B ∈ V    ⇒   ⊢ B ∈ {A, B}
Theorem	prprc1 3469	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ A ∈ V → {A, B} = {B})
Theorem	prprc2 3470	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ B ∈ V → {A, B} = {A})
Theorem	prprc 3471	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ A ∈ V ∧ ¬ B ∈ V) → {A, B} = ∅)
Theorem	tpid1 3472	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ A ∈ V    ⇒   ⊢ A ∈ {A, B, 𝐶}
Theorem	tpid2 3473	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ B ∈ V    ⇒   ⊢ B ∈ {A, B, 𝐶}
Theorem	tpid3g 3474	Closed theorem form of tpid3 3475. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (A ∈ B → A ∈ {𝐶, 𝐷, A})
Theorem	tpid3 3475	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐶 ∈ {A, B, 𝐶}
Theorem	snnzg 3476	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (A ∈ 𝑉 → {A} ≠ ∅)
Theorem	snmg 3477*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ (A ∈ 𝑉 → ∃x x ∈ {A})
Theorem	snnz 3478	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ A ∈ V    ⇒   ⊢ {A} ≠ ∅
Theorem	snm 3479*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
⊢ A ∈ V    ⇒   ⊢ ∃x x ∈ {A}
Theorem	prmg 3480*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ (A ∈ 𝑉 → ∃x x ∈ {A, B})
Theorem	prnz 3481	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ A ∈ V    ⇒   ⊢ {A, B} ≠ ∅
Theorem	prm 3482*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ A ∈ V    ⇒   ⊢ ∃x x ∈ {A, B}
Theorem	prnzg 3483	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
⊢ (A ∈ 𝑉 → {A, B} ≠ ∅)
Theorem	tpnz 3484	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ A ∈ V    ⇒   ⊢ {A, B, 𝐶} ≠ ∅
Theorem	snss 3485	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.)
⊢ A ∈ V    ⇒   ⊢ (A ∈ B ↔ {A} ⊆ B)
Theorem	eldifsn 3486	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (A ∈ (B ∖ {𝐶}) ↔ (A ∈ B ∧ A ≠ 𝐶))
Theorem	eldifsni 3487	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (A ∈ (B ∖ {𝐶}) → A ≠ 𝐶)
Theorem	neldifsn 3488	A is not in (B ∖ {A}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ A ∈ (B ∖ {A})
Theorem	neldifsnd 3489	A is not in (B ∖ {A}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → ¬ A ∈ (B ∖ {A}))
Theorem	rexdifsn 3490	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃x ∈ (A ∖ {B})φ ↔ ∃x ∈ A (x ≠ B ∧ φ))
Theorem	snssg 3491	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.)
⊢ (A ∈ 𝑉 → (A ∈ B ↔ {A} ⊆ B))
Theorem	difsn 3492	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.)
⊢ (¬ A ∈ B → (B ∖ {A}) = B)
Theorem	difprsnss 3493	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ({A, B} ∖ {A}) ⊆ {B}
Theorem	difprsn1 3494	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (A ≠ B → ({A, B} ∖ {A}) = {B})
Theorem	difprsn2 3495	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ (A ≠ B → ({A, B} ∖ {B}) = {A})
Theorem	diftpsn3 3496	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
⊢ ((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A, B})
Theorem	difsnb 3497	(B ∖ {A}) equals B if and only if A is not a member of B. Generalization of difsn 3492. (Contributed by David Moews, 1-May-2017.)
⊢ (¬ A ∈ B ↔ (B ∖ {A}) = B)
Theorem	difsnpssim 3498	(B ∖ {A}) is a proper subclass of B if A is a member of B. In classical logic, the converse holds as well. (Contributed by Jim Kingdon, 9-Aug-2018.)
⊢ (A ∈ B → (B ∖ {A}) ⊊ B)
Theorem	snssi 3499	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
⊢ (A ∈ B → {A} ⊆ B)
Theorem	snssd 3500	The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ∈ B)    ⇒   ⊢ (φ → {A} ⊆ B)