P. 55 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5401-5500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sels 5401*	If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5403. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5254, ax-nul 5264, ax-pow 5323. (Revised by BTernaryTau, 15-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	selsALT 5402*	Alternate proof of sels 5401, requiring ax-sep 5254 but not using el 5400 (which is proved from it as elALT 5403). (especially when the proof of el 5400 is inlined in sels 5401). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5403. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	elALT 5403*	Alternate proof of el 5400, shorter but requiring ax-sep 5254. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	dtruOLD 5404*	Obsolete version of dtru 5399 as of 1-Jan-2025. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2371. (Revised by BJ, 31-May-2019.) Avoid ax-12 2178. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5390 instead of ax-pow 5323. (Revised by BTernaryTau, 3-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	snelpwg 5405	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 5264. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
Theorem	snelpwi 5406	If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	snelpwiOLD 5407	Obsolete version of snelpwi 5406 as of 17-Jan-2025. (Contributed by NM, 28-May-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	snelpw 5408	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)
Theorem	prelpw 5409	An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
Theorem	prelpwi 5410	If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
Theorem	rext 5411*	A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
⊢ (∀𝑧(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)
Theorem	sspwb 5412	The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Theorem	unipw 5413	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
⊢ ∪ 𝒫 𝐴 = 𝐴
Theorem	univ 5414	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
⊢ ∪ V = V
Theorem	pwtr 5415	A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴)
Theorem	ssextss 5416*	An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))
Theorem	ssext 5417*	An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
Theorem	nssss 5418*	Negation of subclass relationship. Compare nss 4014. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))
Theorem	pweqb 5419	Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
⊢ (𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵)
Theorem	intidg 5420*	The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) Put in closed form and avoid ax-nul 5264. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴})
Theorem	intidOLD 5421*	Obsolete version of intidg 5420 as of 18-Jan-2025. (Contributed by NM, 5-Jun-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴}
Theorem	moabex 5422	"At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.)
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	rmorabex 5423	Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	euabex 5424	The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	nnullss 5425*	A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅))
Theorem	exss 5426*	Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑))
Theorem	opex 5427	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ⟨𝐴, 𝐵⟩ ∈ V
Theorem	otex 5428	An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.)
⊢ ⟨𝐴, 𝐵, 𝐶⟩ ∈ V
Theorem	elopg 5429	Characterization of the elements of an ordered pair. Closed form of elop 5430. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵})))
Theorem	elop 5430	Characterization of the elements of an ordered pair. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020.) (Avoid depending on this detail.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ ⟨𝐵, 𝐶⟩ ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶}))
Theorem	opi1 5431	One of the two elements in an ordered pair. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
Theorem	opi2 5432	One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ∈ ⟨𝐴, 𝐵⟩
Theorem	opeluu 5433	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → (𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶))
Theorem	op1stb 5434	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6203 to extract the second member, op1sta 6201 for an alternate version, and op1st 7979 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴
Theorem	brv 5435	Two classes are always in relation by V. This is simply equivalent to ⟨𝐴, 𝐵⟩ ∈ V, and does not imply that V is a relation: see nrelv 5766. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴V𝐵
2.3.3  Ordered pair theorem
Theorem	opnz 5436	An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (⟨𝐴, 𝐵⟩ ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	opnzi 5437	An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ≠ ∅
Theorem	opth1 5438	Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
Theorem	opth 5439	The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthg 5440	Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opth1g 5441	Equality of the first members of equal ordered pairs. Closed form of opth1 5438. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶))
Theorem	opthg2 5442	Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opth2 5443	Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthneg 5444	Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷)))
Theorem	opthne 5445	Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ≠ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷))
Theorem	otth2 5446	Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨⟨𝐴, 𝐵⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	otth 5447	Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	otthg 5448	Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
Theorem	otthne 5449	Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝐶⟩ ≠ ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹))
Theorem	eqvinop 5450*	A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ = ⟨𝐵, 𝐶⟩))
Theorem	sbcop1 5451*	The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑎 / 𝑥]𝜓 ↔ [⟨𝑎, 𝑦⟩ / 𝑧]𝜑)
Theorem	sbcop 5452*	The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of each of its components. (Contributed by AV, 8-Apr-2023.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ [⟨𝑎, 𝑏⟩ / 𝑧]𝜑)
Theorem	copsexgw 5453*	Version of copsexg 5454 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by GG, 26-Jan-2024.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsexg 5454*	Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker copsexgw 5453 when possible. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 25-Aug-2019.) (New usage is discouraged.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsex2t 5455*	Closed theorem form of copsex2g 5456. (Contributed by NM, 17-Feb-2013.)
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2g 5456*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) Use a similar proof to copsex4g 5458 to reduce axiom usage. (Revised by SN, 1-Sep-2024.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2dv 5457*	Implicit substitution deduction for ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ 𝜒))
Theorem	copsex4g 5458*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓))
Theorem	0nelop 5459	A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ¬ ∅ ∈ ⟨𝐴, 𝐵⟩
Theorem	opwo0id 5460	An ordered pair is equal to the ordered pair without the empty set. This is because no ordered pair contains the empty set. (Contributed by AV, 15-Nov-2021.)
⊢ ⟨𝑋, 𝑌⟩ = (⟨𝑋, 𝑌⟩ ∖ {∅})
Theorem	opeqex 5461	Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V)))
Theorem	oteqex2 5462	Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.)
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑅, 𝑆⟩, 𝑇⟩ → (𝐶 ∈ V ↔ 𝑇 ∈ V))
Theorem	oteqex 5463	Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑅, 𝑆⟩, 𝑇⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V)))
Theorem	opcom 5464	An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐵, 𝐴⟩ ↔ 𝐴 = 𝐵)
Theorem	moop2 5465*	"At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∃*𝑥 𝐴 = ⟨𝐵, 𝑥⟩
Theorem	opeqsng 5466	Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})))
Theorem	opeqsn 5467	Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))
Theorem	opeqpr 5468	Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴})))
Theorem	snopeqop 5469	Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({⟨𝐴, 𝐵⟩} = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = {𝐴}))
Theorem	propeqop 5470	Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
Theorem	propssopi 5471	If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶)
Theorem	snopeqopsnid 5472	Equivalence for an ordered pair of two identical singletons equal to a singleton of an ordered pair. (Contributed by AV, 24-Sep-2020.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐴⟩} = ⟨{𝐴}, {𝐴}⟩
Theorem	mosubopt 5473*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
Theorem	mosubop 5474*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
⊢ ∃*𝑥𝜑    ⇒   ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
Theorem	euop2 5475*	Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦(𝑥 = ⟨𝐴, 𝑦⟩ ∧ 𝜑) ↔ ∃!𝑦𝜑)
Theorem	euotd 5476*	Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))    ⇒   ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Theorem	opthwiener 5477	Justification theorem for the ordered pair definition in Norbert Wiener, A simplification of the logic of relations, Proceedings of the Cambridge Philosophical Society, 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e., are not proper classes). See df-op 4599 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	uniop 5478	The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ⟨𝐴, 𝐵⟩ = {𝐴, 𝐵}
Theorem	uniopel 5479	Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → ∪ ⟨𝐴, 𝐵⟩ ∈ ∪ 𝐶)
Theorem	opthhausdorff 5480	Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: ⟨𝐴, 𝐵⟩H = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually, any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5316). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary in full extent (𝐴 ≠ 𝑇 is not required). This definition is meaningful only for classes 𝐴 and 𝐵 that exist as sets (i.e., are not proper classes): If 𝐴 and 𝐶 were different proper classes (𝐴 ≠ 𝐶), then {{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇} ↔ {{𝑂}, {𝐵, 𝑇}} = {{𝑂}, {𝐷, 𝑇} is true if 𝐵 = 𝐷, but (𝐴 = 𝐶 ∧ 𝐵 = 𝐷) would be false. See df-op 4599 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑇    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthhausdorff0 5481	Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: ⟨𝐴, 𝐵⟩H = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually, any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5316). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary if all involved classes exist as sets (i.e. are not proper classes), in contrast to opthhausdorff 5480. See df-op 4599 for other ordered pair definitions. (Contributed by AV, 12-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	otsndisj 5482*	The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {⟨𝐴, 𝐵, 𝑐⟩})
Theorem	otiunsndisj 5483*	The union of singletons consisting of ordered triples which have distinct first and third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){⟨𝑎, 𝐵, 𝑐⟩})
Theorem	iunopeqop 5484*	Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
Theorem	brsnop 5485	Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑋{⟨𝐴, 𝐵⟩}𝑌 ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵)))
Theorem	brtp 5486	A necessary and sufficient condition for two sets to be related under a binary relation which is an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))
2.3.4  Ordered-pair class abstractions (cont.)
Theorem	opabidw 5487*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5488 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2371. (Revised by GG, 26-Jan-2024.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	opabid 5488	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker opabidw 5487 when possible. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	elopabw 5489*	Membership in a class abstraction of ordered pairs. Weaker version of elopab 5490 with a sethood antecedent, avoiding ax-sep 5254, ax-nul 5264, and ax-pr 5390. Originally a subproof of elopab 5490. (Contributed by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	elopab 5490*	Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Theorem	rexopabb 5491*	Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023.)
⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    &   ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑜 ∈ 𝑂 𝜓 ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜒))
Theorem	vopelopabsb 5492*	The law of concretion in terms of substitutions. Version of opelopabsb 5493 with set variables. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Remove unnecessary commutation. (Revised by SN, 1-Sep-2024.)
⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	opelopabsb 5493*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	brabsb 5494*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	opelopabt 5495*	Closed theorem form of opelopab 5505. (Contributed by NM, 19-Feb-2013.)
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	opelopabga 5496*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	brabga 5497*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))
Theorem	opelopab2a 5498*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓))
Theorem	opelopaba 5499*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)
Theorem	braba 5500*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝜓)