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	exel 5401*	There exist two sets, one a member of the other. This theorem looks similar to el 5405, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1841, ax-6 1999, and ax-pr 5390. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5402. (Contributed by SN, 23-Dec-2024.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	exexneq 5402*	There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2401. (Revised by BJ, 31-May-2019.) Avoid ax-8 2146. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2212. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5390 instead of ax-pow 5326. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5404. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦
Theorem	exneq 5403*	Given any set (the "𝑦 " in the statement), there exists a set not equal to it. The same statement without disjoint variable condition is false, since we do not have ∃𝑥¬ 𝑥 = 𝑥. This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext 2732, ax-sep 5248, or ax-pow 5326 nor auxiliary logical axiom schemes ax-10 2177 to ax-13 2401. See dtruALT 5349 for a shorter proof using more axioms, and dtruALT2 5331 for a proof using ax-pow 5326 instead of ax-pr 5390. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2401. (Revised by BJ, 31-May-2019.) Avoid ax-8 2146. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2212. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5390 instead of ax-pow 5326. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5404. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥 ¬ 𝑥 = 𝑦
Theorem	dtru 5404*	Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2060. The same comments and revision history concerning axiom usage as in exneq 5403 apply. See dtruALT 5349 and dtruALT2 5331 for alternate proofs avoiding ax-pr 5390. (Contributed by NM, 7-Nov-2006.) Extract exneq 5403 as an intermediate result. (Revised by BJ, 2-Jan-2025.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	el 5405*	Any set is an element of some other set. See elALT 5409 for a shorter proof using more axioms, and see elALT2 5330 for a proof that uses ax-9 2154 and ax-pow 5326 instead of ax-pr 5390. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5390 instead of ax-9 2154 and ax-pow 5326. (Revised by BTernaryTau, 2-Dec-2024.) (Proof shortened by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	el.OLD 5406*	Obsolete version of el 5405 as of 6-Apr-2026. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	sels 5407*	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 5409. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5248, ax-nul 5259, ax-pow 5326. (Revised by BTernaryTau, 15-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	selsALT 5408*	Alternate proof of sels 5407, requiring ax-sep 5248 but not using el 5405 (which is proved from it as elALT 5409). (especially when the proof of el 5405 is inlined in sels 5407). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5409. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	elALT 5409*	Alternate proof of el 5405, shorter but requiring ax-sep 5248. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	snelpwg 5410	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 5259. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
Theorem	snelpwi 5411	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	snelpw 5412	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 5413	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 5414	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 5415*	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 5416	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 5417	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 5418	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 5419	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 5420*	An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))
Theorem	ssext 5421*	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 5422*	Negation of subclass relationship. Compare nss 3972. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))
Theorem	pweqb 5423	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 5424*	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 5259. (Revised by BJ, 17-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴})
Theorem	moabex 5425	"At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) Avoid axioms. (Revised by SN, 2-Feb-2026.)
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	moabexOLD 5426	Obsolete version of moabex 5425 as of 2-Feb-2026. (Contributed by NM, 30-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	rmorabex 5427	Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	euabex 5428	The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	nnullss 5429*	A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅))
Theorem	exss 5430*	Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑))
Theorem	opex 5431	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.) Avoid ax-nul 5259. (Revised by GG, 6-Mar-2026.)
⊢ ⟨𝐴, 𝐵⟩ ∈ V
Theorem	opexOLD 5432	Obsolete version of opex 5431 as of 6-Mar-2026. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ⟨𝐴, 𝐵⟩ ∈ V
Theorem	otex 5433	An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.)
⊢ ⟨𝐴, 𝐵, 𝐶⟩ ∈ V
Theorem	elopg 5434	Characterization of the elements of an ordered pair. Closed form of elop 5435. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵})))
Theorem	elop 5435	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 5436	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 5437	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 5438	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 5439	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6228 to extract the second member, op1sta 6226 for an alternate version, and op1st 8009 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴
Theorem	brv 5440	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 5776. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴V𝐵
2.3.3  Ordered pair theorem
Theorem	opnz 5441	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 5442	An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ≠ ∅
Theorem	opth1 5443	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 5444	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 5445	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 5446	Equality of the first members of equal ordered pairs. Closed form of opth1 5443. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶))
Theorem	opthg2 5447	Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opth2 5448	Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthneg 5449	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 5450	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 5451	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 5452	Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	otthg 5453	Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
Theorem	otthne 5454	Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝐶⟩ ≠ ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹))
Theorem	eqvinop 5455*	A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ = ⟨𝐵, 𝐶⟩))
Theorem	eqvinot 5456*	A variable introduction law for ordered triples, analogous to eqvinop 5455. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶, 𝐷⟩ ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ ⟨𝑥, 𝑦, 𝑧⟩ = ⟨𝐵, 𝐶, 𝐷⟩))
Theorem	sbcop1 5457*	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 5458*	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 5459*	Version of copsexg 5461 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by GG, 26-Jan-2024.) Shorten proof and remove dependency on ax-10 2177. (Revised by Eric Schmidt, 2-May-2026.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsexgwOLD 5460*	Obsolete version of copsexgw 5459 as of 2-May-2026. (Contributed by GG, 26-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsexg 5461*	Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. Usage of this theorem is discouraged because it depends on ax-13 2401. Use the weaker copsexgw 5459 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	cotsexgw 5462*	Substitution of class 𝐴 for ordered triple ⟨𝑥, 𝑦, 𝑧⟩, analogous to copsexgw 5459. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (𝜑 ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝜑)))
Theorem	copsex2t 5463*	Closed theorem form of copsex2g 5464. (Contributed by NM, 17-Feb-2013.)
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2g 5464*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) Use a similar proof to copsex4g 5466 to reduce axiom usage. (Revised by SN, 1-Sep-2024.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2dv 5465*	Implicit substitution deduction for ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ 𝜒))
Theorem	copsex4g 5466*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓))
Theorem	0nelop 5467	A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ¬ ∅ ∈ ⟨𝐴, 𝐵⟩
Theorem	opwo0id 5468	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 5469	Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V)))
Theorem	oteqex2 5470	Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.)
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑅, 𝑆⟩, 𝑇⟩ → (𝐶 ∈ V ↔ 𝑇 ∈ V))
Theorem	oteqex 5471	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 5472	An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐵, 𝐴⟩ ↔ 𝐴 = 𝐵)
Theorem	moop2 5473*	"At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∃*𝑥 𝐴 = ⟨𝐵, 𝑥⟩
Theorem	opeqsng 5474	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 5475	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 5476	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 5477	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 5478	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 5479	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 5480	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 5481*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
Theorem	mosubop 5482*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
⊢ ∃*𝑥𝜑    ⇒   ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
Theorem	mosubott 5483*	"At most one" remains true inside ordered triple quantification, analogous to mosubopt 5481. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ (∀𝑥∀𝑦∀𝑧∃*𝑤𝜑 → ∃*𝑤∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝜑))
Theorem	euop2 5484*	Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦(𝑥 = ⟨𝐴, 𝑦⟩ ∧ 𝜑) ↔ ∃!𝑦𝜑)
Theorem	euotd 5485*	Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))    ⇒   ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Theorem	opthwiener 5486	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 4835 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	uniop 5487	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 5488	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 5489	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 5318). 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 4835 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑇    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthhausdorff0 5490	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 5318). 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 5489. See df-op 4835 for other ordered pair definitions. (Contributed by AV, 12-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	otsndisj 5491*	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 5492*	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 5493*	Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.) Remove antecedent. (Revised by Eric Schmidt, 9-May-2026.) (Avoid depending on this detail.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧})
Theorem	iunopeqopOLD 5494*	Obsolete version of iunopeqop 5493 as of 9-May-2026. (Contributed by AV, 20-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
Theorem	brsnop 5495	Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑋{⟨𝐴, 𝐵⟩}𝑌 ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵)))
Theorem	brtp 5496	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 5497*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5498 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2401. (Revised by GG, 26-Jan-2024.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	opabid 5498	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 2401. Use the weaker opabidw 5497 when possible. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	elopabw 5499*	Membership in a class abstraction of ordered pairs. Weaker version of elopab 5500 with a sethood antecedent, avoiding ax-sep 5248, ax-nul 5259, and ax-pr 5390. Originally a subproof of elopab 5500. (Contributed by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	elopab 5500*	Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))