P. 49 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ssunpr 4801	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷}))))
Theorem	sspr 4802	The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})))
Theorem	sstp 4803	The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))))
Theorem	tpss 4804	An unordered triple 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 4805	An unordered triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷)
Theorem	sneqrg 4806	Closed form of sneqr 4807. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵))
Theorem	sneqr 4807	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 4808	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵)
Theorem	mosneq 4809*	There exists at most one set whose singleton is equal to a given class. See also moeq 3681. (Contributed by BJ, 24-Sep-2022.)
⊢ ∃*𝑥{𝑥} = 𝐴
Theorem	sneqbg 4810	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵))
Theorem	snsspw 4811	The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.)
⊢ {𝐴} ⊆ 𝒫 𝐴
Theorem	prsspw 4812	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 4813	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 4814	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 4815	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 4816	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 4817	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))
Theorem	opthpr 4818	An unordered pair has the ordered pair property (compare opth 5439) under certain conditions. (Contributed by NM, 27-Mar-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	preqr1g 4819	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4815. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵))
Theorem	preq12bg 4820	Closed form of preq12b 4817. (Contributed by Scott Fenton, 28-Mar-2014.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
Theorem	prneimg 4821	Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Theorem	prneimg2 4822	Two pairs are not equal if their counterparts are not equal. (Contributed by AV, 5-Sep-2025.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} ↔ ((𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷) ∧ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐶))))
Theorem	prnebg 4823	A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
Theorem	pr1eqbg 4824	A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 ↔ {𝐴, 𝐵} = {𝐵, 𝐶}))
Theorem	pr1nebg 4825	A (proper) pair is not equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑋) ∧ 𝐴 ≠ 𝐵) → (𝐴 ≠ 𝐶 ↔ {𝐴, 𝐵} ≠ {𝐵, 𝐶}))
Theorem	preqsnd 4826	Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.) (Revised by AV, 13-Jun-2022.) (Revised by AV, 16-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶)))
Theorem	prnesn 4827	A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≠ {𝐶})
Theorem	prneprprc 4828	A proper unordered pair is not an improper unordered pair. (Contributed by AV, 13-Jun-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ ¬ 𝐶 ∈ V) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})
Theorem	preqsn 4829	Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 12-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
Theorem	preq12nebg 4830	Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))
Theorem	prel12g 4831	Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.) (Revised by AV, 9-Dec-2018.) (Revised by AV, 12-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))
Theorem	opthprneg 4832	An unordered pair has the ordered pair property (compare opth 5439) under certain conditions. Variant of opthpr 4818 in closed form. (Contributed by AV, 13-Jun-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	elpreqprlem 4833*	Lemma for elpreqpr 4834. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥})
Theorem	elpreqpr 4834*	Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.)
⊢ (𝐴 ∈ {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥})
Theorem	elpreqprb 4835*	A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥}))
Theorem	elpr2elpr 4836*	For an element 𝐴 of an unordered pair which is a subset of a given set 𝑉, there is another (maybe the same) element 𝑏 of the given set 𝑉 being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ {𝑋, 𝑌}) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})
Theorem	dfopif 4837	Rewrite df-op 4599 using if. When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
Theorem	dfopg 4838	Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
Theorem	dfop 4839	Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}}
Theorem	opeq1 4840	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Theorem	opeq2 4841	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Theorem	opeq12 4842	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
Theorem	opeq1i 4843	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩
Theorem	opeq2i 4844	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩
Theorem	opeq12i 4845	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩
Theorem	opeq1d 4846	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Theorem	opeq2d 4847	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Theorem	opeq12d 4848	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Theorem	oteq1 4849	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
Theorem	oteq2 4850	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
Theorem	oteq3 4851	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Theorem	oteq1d 4852	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐷⟩ = ⟨𝐵, 𝐶, 𝐷⟩)
Theorem	oteq2d 4853	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐴, 𝐷⟩ = ⟨𝐶, 𝐵, 𝐷⟩)
Theorem	oteq3d 4854	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Theorem	oteq123d 4855	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐶, 𝐸⟩ = ⟨𝐵, 𝐷, 𝐹⟩)
Theorem	nfop 4856	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟨𝐴, 𝐵⟩
Theorem	nfopd 4857	Deduction version of bound-variable hypothesis builder nfop 4856. This shows how the deduction version of a not-free theorem such as nfop 4856 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥⟨𝐴, 𝐵⟩)
Theorem	csbopg 4858	Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⟨𝐶, 𝐷⟩ = ⟨⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟩)
Theorem	opidg 4859	The ordered pair ⟨𝐴, 𝐴⟩ in Kuratowski's representation. Closed form of opid 4860. (Contributed by Peter Mazsa, 22-Jul-2019.) (Avoid depending on this detail.)
⊢ (𝐴 ∈ 𝑉 → ⟨𝐴, 𝐴⟩ = {{𝐴}})
Theorem	opid 4860	The ordered pair ⟨𝐴, 𝐴⟩ in Kuratowski's representation. Inference form of opidg 4859. (Contributed by FL, 28-Dec-2011.) (Proof shortened by AV, 16-Feb-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐴⟩ = {{𝐴}}
Theorem	ralunsn 4861*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)))
Theorem	2ralunsn 4862*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃))))
Theorem	opprc 4863	Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc1 4864	Expansion of an ordered pair when the first member is a proper class. See also opprc 4863. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	opprc2 4865	Expansion of an ordered pair when the second member is a proper class. See also opprc 4863. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (¬ 𝐵 ∈ V → ⟨𝐴, 𝐵⟩ = ∅)
Theorem	oprcl 4866	If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐶 ∈ ⟨𝐴, 𝐵⟩ → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pwsn 4867	The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
⊢ 𝒫 {𝐴} = {∅, {𝐴}}
Theorem	pwpr 4868	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}})
Theorem	pwtp 4869	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}}))
Theorem	pwpwpw0 4870	Compute the power set of the power set of the power set of the empty set. (See also pw0 4779 and pwpw0 4780.) (Contributed by NM, 2-May-2009.)
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}})
Theorem	pwv 4871	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. The collection of all classes is of course larger than V, which is the collection of all sets. But 𝒫 V, being a class, cannot contain proper classes, so 𝒫 V is actually no larger than V. This fact is exploited in ncanth 7345. (Contributed by NM, 14-Sep-2003.)
⊢ 𝒫 V = V
Theorem	prproe 4872*	For an element of a proper unordered pair of elements of a class 𝑉, there is another (different) element of the class 𝑉 which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.)
⊢ ((𝐶 ∈ {𝐴, 𝐵} ∧ 𝐴 ≠ 𝐵 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∃𝑣 ∈ (𝑉 ∖ {𝐶})𝑣 ∈ {𝐴, 𝐵})
Theorem	3elpr2eq 4873	If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021.)
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍)
2.1.19  The union of a class
Syntax	cuni 4874	Extend class notation to include the union of a class. Read: "union (of) 𝐴".
class ∪ 𝐴
Definition	df-uni 4875*	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 30362). This is similar to the union of two classes df-un 3922. (Contributed by NM, 23-Aug-1993.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
Theorem	dfuni2 4876*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
Theorem	eluni 4877*	Membership in class union. (Contributed by NM, 22-May-1994.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	eluni2 4878*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	elunii 4879	Membership in class union. (Contributed by NM, 24-Mar-1995.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶)
Theorem	nfunid 4880	Deduction version of nfuni 4881. (Contributed by NM, 18-Feb-2013.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴)
Theorem	nfuni 4881	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥∪ 𝐴
Theorem	uniss 4882	Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unissi 4883	Subclass relationship for subclass union. Inference form of uniss 4882. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ∪ 𝐴 ⊆ ∪ 𝐵
Theorem	unissd 4884	Subclass relationship for subclass union. Deduction form of uniss 4882. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)
Theorem	unieq 4885	Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by BJ, 13-Apr-2024.)
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
Theorem	unieqi 4886	Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝐴 = ∪ 𝐵
Theorem	unieqd 4887	Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)
Theorem	eluniab 4888*	Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	elunirab 4889*	Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑))
Theorem	uniprg 4890	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) Avoid using unipr 4891 to prove it from uniprg 4890. (Revised by BJ, 1-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
Theorem	unipr 4891	The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) (Proof shortened by BJ, 1-Sep-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
Theorem	unisng 4892	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴)
Theorem	unisn 4893	A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴
Theorem	unisnv 4894	A set equals the union of its singleton (setvar case). (Contributed by NM, 30-Aug-1993.)
⊢ ∪ {𝑥} = 𝑥
Theorem	unisn3 4895*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴)
Theorem	dfnfc2 4896*	An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴))
Theorem	uniun 4897	The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)
Theorem	uniin 4898	The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 8773 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵)
Theorem	ssuni 4899	Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶)
Theorem	uni0b 4900	The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅})