P. 56 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5501-5600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	otsndisj 5501*	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 5502*	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 5503*	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 5504*	Obsolete version of iunopeqop 5503 as of 9-May-2026. (Contributed by AV, 20-Sep-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (𝐴 ≠ ∅ → (∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} = ⟨𝐶, 𝐷⟩ → ∃𝑧 𝐴 = {𝑧}))
Theorem	brsnop 5505	Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑋{⟨𝐴, 𝐵⟩}𝑌 ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵)))
Theorem	brtp 5506	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 5507*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5508 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	opabid 5508	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 2403. Use the weaker opabidw 5507 when possible. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	elopabw 5509*	Membership in a class abstraction of ordered pairs. Weaker version of elopab 5510 with a sethood antecedent, avoiding ax-sep 5256, ax-nul 5268, and ax-pr 5403. Originally a subproof of elopab 5510. (Contributed by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	elopab 5510*	Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Theorem	rexopabb 5511*	Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023.)
⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    &   ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑜 ∈ 𝑂 𝜓 ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜒))
Theorem	vopelopabsb 5512*	The law of concretion in terms of substitutions. Version of opelopabsb 5513 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 5513*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	brabsb 5514*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	opelopabt 5515*	Closed theorem form of opelopab 5526. (Contributed by NM, 19-Feb-2013.)
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	opelopabga 5516*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	brabga 5517*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))
Theorem	opelopab2a 5518*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓))
Theorem	opelopaba 5519*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)
Theorem	braba 5520*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝜓)
Theorem	brab2d 5521*	Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑉) ∧ 𝜓)})    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒)))
Theorem	opelopabg 5522*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	brabg 5523*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))
Theorem	opelopabgf 5524*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 5522 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	opelopab2 5525*	Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒))
Theorem	opelopab 5526*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)
Theorem	brab 5527*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝜒)
Theorem	opelopabaf 5528*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5526 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)
Theorem	opelopabf 5529*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 5526 uses bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)
Theorem	ssopab2 5530	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	ssopab2bw 5531*	Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b 5533 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by NM, 27-Dec-1996.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	eqopab2bw 5532*	Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b 5536 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-13 2403. (Revised by GG, 26-Jan-2024.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓))
Theorem	ssopab2b 5533	Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker ssopab2bw 5531 when possible. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (New usage is discouraged.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	ssopab2i 5534	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	ssopab2dv 5535*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	eqopab2b 5536	Equivalence of ordered pair abstraction equality and biconditional. Usage of this theorem is discouraged because it depends on ax-13 2403. Use the weaker eqopab2bw 5532 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓))
Theorem	opabn0 5537	Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑)
Theorem	opab0 5538	Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	csbopab 5539*	Move substitution into a class abstraction. Version of csbopabw 5540 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}
Theorem	csbopabw 5540*	Move substitution into a class abstraction. Version of csbopab 5539 with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpt12 5541*	Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍))
Theorem	csbmpt2 5542*	Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍))
Theorem	iunopab 5543*	Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) Avoid ax-sep 5256, ax-nul 5268, ax-pr 5403. (Revised by SN, 11-Nov-2024.)
⊢ ∪ 𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 𝜑}
Theorem	elopabr 5544*	Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅)
Theorem	elopabran 5545*	Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅)
Theorem	rbropapd 5546*	Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))))
Theorem	rbropap 5547*	Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))
Theorem	2rbropap 5548*	Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the conditions 𝜓 and 𝜏. (Contributed by AV, 31-Jan-2021.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓 ∧ 𝜏)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜏 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒 ∧ 𝜃)))
Theorem	0nelopab 5549	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024.)
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	brabv 5550	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
⊢ (𝑋{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V))
2.3.5  Power class of union and intersection
Theorem	pwin 5551	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵)
Theorem	pwssun 5552	The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Theorem	pwun 5553	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))
2.3.6  The identity relation
Syntax	cid 5554	Extend the definition of a class to include the identity relation.
class I
Definition	df-id 5555*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 30796). (Contributed by NM, 13-Aug-1995.)
⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
Theorem	dfid4 5556	The identity function expressed using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ I = (𝑥 ∈ V ↦ 𝑥)
Theorem	dfid2 5557	Alternate definition of the identity relation. Instance of dfid3 5558 not requiring auxiliary axioms. (Contributed by NM, 15-Mar-2007.) Reduce axiom usage. (Revised by GG, 4-Nov-2024.) (Proof shortened by BJ, 5-Nov-2024.) Use df-id 5555 instead to make the semantics of the constructor df-opab 5173 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ 𝑥 = 𝑥}
Theorem	dfid3 5558	A stronger version of df-id 5555 that does not require 𝑥 and 𝑦 to be disjoint. This is not the definition since, in order to pass our definition soundness test, a definition has to have disjoint dummy variables, see conventions 30762. The proof can be instructive in showing how disjoint variable conditions may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.) Use df-id 5555 instead to make the semantics of the constructor df-opab 5173 clearer (in usages, 𝑥, 𝑦 will typically be dummy variables, so can be assumed disjoint). (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
2.3.7  The membership relation (or epsilon relation)
Syntax	cep 5559	Extend class notation to include the membership relation.
class E
Definition	df-eprel 5560*	Define the membership relation (also called "epsilon relation" since it is sometimes denoted by the lowercase Greek letter "epsilon"). Similar to Definition 6.22 of [TakeutiZaring] p. 30. The membership relation and the membership predicate agree, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵), when 𝐵 is a set (see epelg 5561). Thus, ⊢ 5 E {1, 5} (ex-eprel 30795). (Contributed by NM, 13-Aug-1995.)
⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
Theorem	epelg 5561	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5563 and closed form of epeli 5562. Definition 1.6 of [Schloeder] p. 1. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 14-Jul-2023.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	epeli 5562	The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5561. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	epel 5563	The membership relation and the membership predicate agree when the "containing" class is a setvar. Definition 1.6 of [Schloeder] p. 1. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.)
⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)
Theorem	0sn0ep 5564	An example for the membership relation. (Contributed by AV, 19-Jun-2022.)
⊢ ∅ E {∅}
Theorem	epn0 5565	The membership relation is nonempty. (Contributed by AV, 19-Jun-2022.)
⊢ E ≠ ∅
2.3.8  Partial and total orderings We have not yet defined relations (df-rel 5667), but here we introduce a few related notions we will use to develop ordinals. The class variable 𝑅 is no different from other class variables, but it reminds us that typically it represents what we will later call a "relation".
Syntax	wpo 5566	Extend wff notation to include the strict partial ordering predicate. Read: "𝑅 is a partial order on 𝐴".
wff 𝑅 Po 𝐴
Syntax	wor 5567	Extend wff notation to include the strict total ordering predicate. Read: "𝑅 orders 𝐴".
wff 𝑅 Or 𝐴
Definition	df-po 5568*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 30797). (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Definition	df-so 5569*	Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11296). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	poss 5570	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	poeq1 5571	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴))
Theorem	poeq2 5572	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵))
Theorem	poeq12d 5573	Equality deduction for partial orderings. (Contributed by Matthew House, 10-Sep-2025.)
⊢ (𝜑 → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵))
Theorem	nfpo 5574	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Po 𝐴
Theorem	nfso 5575	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Or 𝐴
Theorem	pocl 5576	Characteristic properties of a partial order in class notation. (Contributed by NM, 27-Mar-1997.) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024.)
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
Theorem	ispod 5577*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	swopolem 5578*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌)))
Theorem	swopo 5579*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	poirr 5580	A partial order is irreflexive. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	potr 5581	A partial order is a transitive relation. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	po2nr 5582	A partial order has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	po3nr 5583	A partial order has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	po2ne 5584	Two sets related by a partial order are not equal. (Contributed by AV, 13-Mar-2023.)
⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵)
Theorem	po0 5585	Any relation is a partial order on the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝑅 Po ∅
Theorem	pofun 5586*	The inverse image of a partial order is a partial order. (Contributed by Jeff Madsen, 18-Jun-2011.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}    &   ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)    ⇒   ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)
Theorem	sopo 5587	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
Theorem	soss 5588	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	soeq1 5589	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
Theorem	soeq2 5590	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
Theorem	soeq12d 5591	Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) (Proof shortened by Matthew House, 10-Sep-2025.)
⊢ (𝜑 → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵))
Theorem	sonr 5592	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	sotr 5593	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	sotrd 5594	Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    &   ⊢ (𝜑 → 𝑌𝑅𝑍)    ⇒   ⊢ (𝜑 → 𝑋𝑅𝑍)
Theorem	solin 5595	A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))
Theorem	so2nr 5596	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	so3nr 5597	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	sotric 5598	A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotrieq 5599	Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotrieq2 5600	Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵)))