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	prex 5401	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 4728), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5264 and shorten proof. (Revised by GG, 6-Mar-2026.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	snex 5402	A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation and Pairing. See also snexALT 5350. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Avoid ax-nul 5264 and shorten proof. (Revised by GG, 6-Mar-2026.)
⊢ {𝐴} ∈ V
Theorem	snexg 5403	A singleton built on a set is a set. Special case of snex 5402 which is intuitionistically valid. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5402 and shorten proof. (Revised by BJ, 15-Jan-2025.) (Proof shortened by GG, 6-Mar-2026.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snexgALT 5404	Alternate proof of snexg 5403 based on vsnex 5398, which uses an instance of ax-sep 5253. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5402 and shorten proof. (Revised by BJ, 15-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snexOLD 5405	Obsolete version of snex 5402 as of 6-Mar-2026. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴} ∈ V
Theorem	prexOLD 5406	Obsolete version of prex 5401 as of 6-Mar-2026. (Contributed by NM, 15-Jul-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	exel 5407*	There exist two sets, one a member of the other. This theorem looks similar to el 5411, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1842, ax-6 2002, and ax-pr 5396. 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 5408. (Contributed by SN, 23-Dec-2024.)
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦
Theorem	exexneq 5408*	There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2404. (Revised by BJ, 31-May-2019.) Avoid ax-8 2149. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2216. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5396 instead of ax-pow 5332. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5410. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦
Theorem	exneq 5409*	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 2735, ax-sep 5253, or ax-pow 5332 nor auxiliary logical axiom schemes ax-10 2180 to ax-13 2404. See dtruALT 5355 for a shorter proof using more axioms, and dtruALT2 5337 for a proof using ax-pow 5332 instead of ax-pr 5396. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2404. (Revised by BJ, 31-May-2019.) Avoid ax-8 2149. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2216. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5396 instead of ax-pow 5332. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5410. (Revised by BJ, 2-Jan-2025.)
⊢ ∃𝑥 ¬ 𝑥 = 𝑦
Theorem	dtru 5410*	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 2063. The same comments and revision history concerning axiom usage as in exneq 5409 apply. See dtruALT 5355 and dtruALT2 5337 for alternate proofs avoiding ax-pr 5396. (Contributed by NM, 7-Nov-2006.) Extract exneq 5409 as an intermediate result. (Revised by BJ, 2-Jan-2025.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	el 5411*	Any set is an element of some other set. See elALT 5415 for a shorter proof using more axioms, and see elALT2 5336 for a proof that uses ax-9 2157 and ax-pow 5332 instead of ax-pr 5396. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5396 instead of ax-9 2157 and ax-pow 5332. (Revised by BTernaryTau, 2-Dec-2024.) (Proof shortened by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	el.OLD 5412*	Obsolete version of el 5411 as of 6-Apr-2026. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	sels 5413*	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 5415. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5253, ax-nul 5264, ax-pow 5332. (Revised by BTernaryTau, 15-Jan-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	selsALT 5414*	Alternate proof of sels 5413, requiring ax-sep 5253 but not using el 5411 (which is proved from it as elALT 5415). (especially when the proof of el 5411 is inlined in sels 5413). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5415. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	elALT 5415*	Alternate proof of el 5411, shorter but requiring ax-sep 5253. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	snelpwg 5416	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 5417	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 5418	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 5419	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 5420	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 5421*	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 5422	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 5423	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 5424	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 5425	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 5426*	An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))
Theorem	ssext 5427*	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 5428*	Negation of subclass relationship. Compare nss 3977. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))
Theorem	pweqb 5429	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 5430*	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	moabex 5431	"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 5432	Obsolete version of moabex 5431 as of 2-Feb-2026. (Contributed by NM, 30-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	rmorabex 5433	Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	euabex 5434	The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	nnullss 5435*	A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅))
Theorem	exss 5436*	Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑))
Theorem	opex 5437	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 5264. (Revised by GG, 6-Mar-2026.)
⊢ ⟨𝐴, 𝐵⟩ ∈ V
Theorem	opexOLD 5438	Obsolete version of opex 5437 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 5439	An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.)
⊢ ⟨𝐴, 𝐵, 𝐶⟩ ∈ V
Theorem	elopg 5440	Characterization of the elements of an ordered pair. Closed form of elop 5441. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵})))
Theorem	elop 5441	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 5442	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 5443	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 5444	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 5445	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6242 to extract the second member, op1sta 6240 for an alternate version, and op1st 8036 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ ∩ ⟨𝐴, 𝐵⟩ = 𝐴
Theorem	brv 5446	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 5783. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴V𝐵
2.3.3  Ordered pair theorem
Theorem	opnz 5447	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 5448	An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ≠ ∅
Theorem	opth1 5449	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 5450	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 5451	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 5452	Equality of the first members of equal ordered pairs. Closed form of opth1 5449. (Contributed by AV, 14-Oct-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶))
Theorem	opthg2 5453	Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opth2 5454	Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthneg 5455	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 5456	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 5457	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 5458	Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	otthg 5459	Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (⟨𝐴, 𝐵, 𝐶⟩ = ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹)))
Theorem	otthne 5460	Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝐶⟩ ≠ ⟨𝐷, 𝐸, 𝐹⟩ ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹))
Theorem	eqvinop 5461*	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 5462*	A variable introduction law for ordered triples, analogous to eqvinop 5461. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶, 𝐷⟩ ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ ⟨𝑥, 𝑦, 𝑧⟩ = ⟨𝐵, 𝐶, 𝐷⟩))
Theorem	sbcop1 5463*	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 5464*	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 5465*	Version of copsexg 5467 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by GG, 26-Jan-2024.) Shorten proof and remove dependency on ax-10 2180. (Revised by Eric Schmidt, 2-May-2026.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsexgwOLD 5466*	Obsolete version of copsexgw 5465 as of 2-May-2026. (Contributed by GG, 26-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsexg 5467*	Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker copsexgw 5465 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 5468*	Substitution of class 𝐴 for ordered triple ⟨𝑥, 𝑦, 𝑧⟩, analogous to copsexgw 5465. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ (𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ → (𝜑 ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝜑)))
Theorem	copsex2t 5469*	Closed theorem form of copsex2g 5470. (Contributed by NM, 17-Feb-2013.)
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2g 5470*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) Use a similar proof to copsex4g 5472 to reduce axiom usage. (Revised by SN, 1-Sep-2024.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2dv 5471*	Implicit substitution deduction for ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ 𝜒))
Theorem	copsex4g 5472*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓))
Theorem	0nelop 5473	A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ¬ ∅ ∈ ⟨𝐴, 𝐵⟩
Theorem	opwo0id 5474	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 5475	Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V)))
Theorem	oteqex2 5476	Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.)
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑅, 𝑆⟩, 𝑇⟩ → (𝐶 ∈ V ↔ 𝑇 ∈ V))
Theorem	oteqex 5477	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 5478	An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐵, 𝐴⟩ ↔ 𝐴 = 𝐵)
Theorem	moop2 5479*	"At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∃*𝑥 𝐴 = ⟨𝐵, 𝑥⟩
Theorem	opeqsng 5480	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 5481	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 5482	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 5483	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 5484	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 5485	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 5486	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 5487*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑦∀𝑧∃*𝑥𝜑 → ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
Theorem	mosubop 5488*	"At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
⊢ ∃*𝑥𝜑    ⇒   ⊢ ∃*𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
Theorem	mosubott 5489*	"At most one" remains true inside ordered triple quantification, analogous to mosubopt 5487. (Contributed by BTernaryTau, 8-Sep-2026.)
⊢ (∀𝑥∀𝑦∀𝑧∃*𝑤𝜑 → ∃*𝑤∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝜑))
Theorem	euop2 5490*	Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∃!𝑥∃𝑦(𝑥 = ⟨𝐴, 𝑦⟩ ∧ 𝜑) ↔ ∃!𝑦𝜑)
Theorem	euotd 5491*	Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))    ⇒   ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Theorem	opthwiener 5492	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 4839 for other ordered pair definitions. (Contributed by NM, 28-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	uniop 5493	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 5494	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 5495	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 5324). 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 4839 for other ordered pair definitions. (Contributed by AV, 14-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑂    &   ⊢ 𝐵 ≠ 𝑇    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthhausdorff0 5496	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 5324). 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 5495. See df-op 4839 for other ordered pair definitions. (Contributed by AV, 12-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑂 ∈ V    &   ⊢ 𝑇 ∈ V    &   ⊢ 𝑂 ≠ 𝑇    ⇒   ⊢ ({{𝐴, 𝑂}, {𝐵, 𝑇}} = {{𝐶, 𝑂}, {𝐷, 𝑇}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	otsndisj 5497*	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 5498*	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 5499*	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 5500*	Obsolete version of iunopeqop 5499 as of 9-May-2026. (Contributed by AV, 20-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))