P. 47 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4601-4700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ralsnsg 4601*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑))
Theorem	rexsns 4602*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)
Theorem	rexsngf 4603*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	ralsngf 4604*	Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	reusngf 4605*	Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	ralsng 4606*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2139, ax-12 2173. (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	rexsng 4607*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2139, ax-12 2173. (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	reusng 4608*	Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	2ralsng 4609*	Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐵}𝜑 ↔ 𝜒))
Theorem	ralsngOLD 4610*	Obsolete version of ralsng 4606 as of 30-Sep-2024. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	rexsngOLD 4611*	Obsolete version of rexsng 4607 as of 30-Sep-2024. (Contributed by NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
Theorem	rexreusng 4612*	Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑))
Theorem	exsnrex 4613	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 4614*	Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	rexsn 4615*	Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)
Theorem	elpwunsn 4616	Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.)
⊢ (𝐴 ∈ (𝒫 (𝐵 ∪ {𝐶}) ∖ 𝒫 𝐵) → 𝐶 ∈ 𝐴)
Theorem	eqoreldif 4617	An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 ↔ (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵}))))
Theorem	eltpg 4618	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
Theorem	eldiftp 4619	Membership in a set with three elements removed. Similar to eldifsn 4717 and eldifpr 4590. (Contributed by David A. Wheeler, 22-Jul-2017.)
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸)))
Theorem	eltpi 4620	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
Theorem	eltp 4621	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 4622*	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 4623	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥{𝐴, 𝐵}
Theorem	ifpr 4624	Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → if(𝜑, 𝐴, 𝐵) ∈ {𝐴, 𝐵})
Theorem	ralprgf 4625*	Convert a restricted universal quantification over a pair to a conjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 8-Apr-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	rexprgf 4626*	Convert a restricted existential quantification over a pair to a disjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 2-Apr-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)))
Theorem	ralprg 4627*	Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2139, ax-12 2173. (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	ralprgOLD 4628*	Obsolete version of ralprg 4627 as of 30-Sep-2024. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
Theorem	rexprg 4629*	Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2139, ax-12 2173. (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)))
Theorem	rexprgOLD 4630*	Obsolete version of rexprg 4629 as of 30-Sep-2024. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)))
Theorem	raltpg 4631*	Convert a restricted universal quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)))
Theorem	rextpg 4632*	Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)))
Theorem	ralpr 4633*	Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	rexpr 4634*	Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))
Theorem	reuprg0 4635*	Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵)))))
Theorem	reuprg 4636*	Convert a restricted existential uniqueness over a pair to a disjunction and an implication . (Contributed by AV, 2-Apr-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵))))
Theorem	reurexprg 4637*	Convert a restricted existential uniqueness over a pair to a restricted existential quantification and an implication . (Contributed by AV, 3-Apr-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵))))
Theorem	raltp 4638*	Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	rextp 4639*	Convert an existential quantification over an unordered triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃))    ⇒   ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))
Theorem	nfsn 4640	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝐴}
Theorem	csbsng 4641	Distribute proper substitution through the singleton of a class. csbsng 4641 is derived from the virtual deduction proof csbsngVD 42402. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})
Theorem	csbprg 4642	Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
⊢ (𝐶 ∈ 𝑉 → ⦋𝐶 / 𝑥⦌{𝐴, 𝐵} = {⦋𝐶 / 𝑥⦌𝐴, ⦋𝐶 / 𝑥⦌𝐵})
Theorem	elinsn 4643	If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∩ 𝐶) = {𝐴}) → (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
Theorem	disjsn 4644	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 4645	Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.)
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅)
Theorem	disjpr2 4646	Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)
Theorem	disjprsn 4647	The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅)
Theorem	disjtpsn 4648	The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021.)
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷}) = ∅)
Theorem	disjtp2 4649	Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021.)
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸, 𝐹}) = ∅)
Theorem	snprc 4650	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, 21-Jun-1993.)
⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
Theorem	snnzb 4651	A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
Theorem	rmosn 4652*	A restricted at-most-one quantifier over a singleton is always true. (Contributed by AV, 3-Apr-2023.)
⊢ ∃*𝑥 ∈ {𝐴}𝜑
Theorem	r19.12sn 4653*	Special case of r19.12 3252 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 18-Mar-2020.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑))
Theorem	rabsn 4654*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.) (Proof shortened by AV, 26-Aug-2022.)
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵})
Theorem	rabsnifsb 4655*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.)
⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if([𝐴 / 𝑥]𝜑, {𝐴}, ∅)
Theorem	rabsnif 4656*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if(𝜓, {𝐴}, ∅)
Theorem	rabrsn 4657*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Proof shortened by AV, 21-Jul-2019.)
⊢ (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴}))
Theorem	euabsn2 4658*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦})
Theorem	euabsn 4659	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥})
Theorem	reusn 4660*	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 4661	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑)
Theorem	rabsneu 4662	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑)
Theorem	eusn 4663*	Two ways to express "𝐴 is a singleton". (Contributed by NM, 30-Oct-2010.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	rabsnt 4664*	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 4665	Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
⊢ {𝐴, 𝐵} = {𝐵, 𝐴}
Theorem	preq1 4666	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2 4667	Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12 4668	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Theorem	preq1i 4669	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐶}
Theorem	preq2i 4670	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}
Theorem	preq12i 4671	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ {𝐴, 𝐶} = {𝐵, 𝐷}
Theorem	preq1d 4672	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})
Theorem	preq2d 4673	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Theorem	preq12d 4674	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐷})
Theorem	tpeq1 4675	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2 4676	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3 4677	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
⊢ (𝐴 = 𝐵 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq1d 4678	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐷} = {𝐵, 𝐶, 𝐷})
Theorem	tpeq2d 4679	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐴, 𝐷} = {𝐶, 𝐵, 𝐷})
Theorem	tpeq3d 4680	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐶, 𝐷, 𝐴} = {𝐶, 𝐷, 𝐵})
Theorem	tpeq123d 4681	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Theorem	tprot 4682	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
Theorem	tpcoma 4683	Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
Theorem	tpcomb 4684	Swap 2nd and 3rd members of an unordered triple. (Contributed by NM, 22-May-2015.)
⊢ {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
Theorem	tpass 4685	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴} ∪ {𝐵, 𝐶})
Theorem	qdass 4686	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴, 𝐵, 𝐶} ∪ {𝐷})
Theorem	qdassr 4687	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({𝐴, 𝐵} ∪ {𝐶, 𝐷}) = ({𝐴} ∪ {𝐵, 𝐶, 𝐷})
Theorem	tpidm12 4688	Unordered triple {𝐴, 𝐴, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm13 4689	Unordered triple {𝐴, 𝐵, 𝐴} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
Theorem	tpidm23 4690	Unordered triple {𝐴, 𝐵, 𝐵} is just an overlong way to write {𝐴, 𝐵}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
Theorem	tpidm 4691	Unordered triple {𝐴, 𝐴, 𝐴} is just an overlong way to write {𝐴}. (Contributed by David A. Wheeler, 10-May-2015.)
⊢ {𝐴, 𝐴, 𝐴} = {𝐴}
Theorem	tppreq3 4692	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 4693	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 4694	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 4695	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 4696	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4694 and ax-mp 5 has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ 𝐵 ∈ {𝐴, 𝐵}
Theorem	ifpprsnss 4697	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 4698	A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993.)
⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
Theorem	prprc2 4699	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
Theorem	prprc 4700	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ ((¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = ∅)