P. 59 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relopabi 5801	A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5266, ax-nul 5276, ax-pr 5402. (Revised by KP, 25-Oct-2021.)
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ Rel 𝐴
Theorem	relopabiALT 5802	Alternate proof of relopabi 5801 (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ Rel 𝐴
Theorem	relopab 5803	A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) Remove disjoint variable conditions. (Revised by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	mptrel 5804	The maps-to notation always describes a binary relation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	reli 5805	The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ Rel I
Theorem	rele 5806	The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ Rel E
Theorem	opabid2 5807*	A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
⊢ (Rel 𝐴 → {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝐴} = 𝐴)
Theorem	inopab 5808*	Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	difopab 5809*	Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof shortened by SN, 19-Dec-2024.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	difopabOLD 5810*	Obsolete version of difopab 5809 as of 19-Dec-2024. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	inxp 5811	Intersection of two Cartesian products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-10 2141, ax-12 2177. (Revised by SN, 5-May-2025.)
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))
Theorem	inxpOLD 5812	Obsolete version of inxp 5811 as of 5-May-2025. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))
Theorem	xpindi 5813	Distributive law for Cartesian product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶))
Theorem	xpindir 5814	Distributive law for Cartesian product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶))
Theorem	xpiindi 5815*	Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))
Theorem	xpriindi 5816*	Distributive law for Cartesian product over relativized indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐶 × (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))
Theorem	eliunxp 5817*	Membership in a union of Cartesian products. Analogue of elxp 5677 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
Theorem	opeliunxp2 5818*	Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸)    ⇒   ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))
Theorem	raliunxp 5819*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 5821, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
Theorem	rexiunxp 5820*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 5822, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	ralxp 5821*	Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
Theorem	rexxp 5822*	Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	exopxfr 5823*	Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (V × V)𝜑 ↔ ∃𝑦∃𝑧𝜓)
Theorem	exopxfr2 5824*	Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (Rel 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝐴 ∧ 𝜓)))
Theorem	djussxp 5825*	Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
Theorem	ralxpf 5826*	Version of ralxp 5821 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
Theorem	rexxpf 5827*	Version of rexxp 5822 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	iunxpf 5828*	Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)    ⇒   ⊢ ∪ 𝑥 ∈ (𝐴 × 𝐵)𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑧 ∈ 𝐵 𝐷
Theorem	opabbi2dv 5829*	Deduce equality of a relation and an ordered-pair class abstraction. Compare eqabdv 2868. (Contributed by NM, 24-Feb-2014.)
⊢ Rel 𝐴    &   ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	relop 5830*	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg 5782, as funsng 6586 is to funop 7138. (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
Theorem	ideqg 5831	For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	ideq 5832	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)
Theorem	ididg 5833	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
Theorem	issetid 5834	Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ V ↔ 𝐴 I 𝐴)
Theorem	coss1 5835	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
Theorem	coss2 5836	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
Theorem	coeq1 5837	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2 5838	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq1i 5839	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)
Theorem	coeq2i 5840	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)
Theorem	coeq1d 5841	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2d 5842	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq12i 5843	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)
Theorem	coeq12d 5844	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))
Theorem	nfco 5845	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵)
Theorem	brcog 5846*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
Theorem	opelco2g 5847*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶)))
Theorem	brcogw 5848	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵)
Theorem	eqbrrdva 5849*	Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷))    &   ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	brco 5850*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	opelco 5851*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	cnvss 5852	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.)
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
Theorem	cnveq 5853	Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.)
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
Theorem	cnveqi 5854	Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ◡𝐴 = ◡𝐵
Theorem	cnveqd 5855	Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ◡𝐴 = ◡𝐵)
Theorem	elcnv 5856*	Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥))
Theorem	elcnv2 5857*	Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
Theorem	nfcnv 5858	Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥◡𝐴
Theorem	brcnvg 5859	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	opelcnvg 5860	Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
Theorem	opelcnv 5861	Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Theorem	brcnv 5862	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	csbcnv 5863	Move class substitution in and out of the converse of a relation. Version of csbcnvgALT 5864 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.)
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹
Theorem	csbcnvgALT 5864	Move class substitution in and out of the converse of a relation. Version of csbcnv 5863 with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹)
Theorem	cnvco 5865	Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)
Theorem	cnvuni 5866*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
Theorem	dfdm3 5867*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	dfrn2 5868*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	dfrn3 5869*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	elrn2g 5870*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	elrng 5871*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
Theorem	elrn2 5872*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)
Theorem	elrn 5873*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)
Theorem	ssrelrn 5874*	If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.)
⊢ ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎 ∈ 𝐴 𝑎𝑅𝑌)
Theorem	dfdm4 5875	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = ran ◡𝐴
Theorem	dfdmf 5876*	Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
Theorem	csbdm 5877	Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) (Revised by NM, 24-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵
Theorem	eldmg 5878*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Theorem	eldm2g 5879*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
Theorem	eldm 5880*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Theorem	eldm2 5881*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)
Theorem	dmss 5882	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
Theorem	dmeq 5883	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Theorem	dmeqi 5884	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ dom 𝐴 = dom 𝐵
Theorem	dmeqd 5885	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐴 = dom 𝐵)
Theorem	opeldmd 5886	Membership of first of an ordered pair in a domain. Deduction version of opeldm 5887. (Contributed by AV, 11-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶))
Theorem	opeldm 5887	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)
Theorem	breldm 5888	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	breldmg 5889	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	dmun 5890	The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)
Theorem	dmin 5891	The domain of an intersection is included in the intersection of the domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
⊢ dom (𝐴 ∩ 𝐵) ⊆ (dom 𝐴 ∩ dom 𝐵)
Theorem	breldmd 5892	Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
Theorem	dmiun 5893	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	dmuni 5894*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	dmopab 5895*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Theorem	dmopabelb 5896*	A set is an element of the domain of an ordered pair class abstraction iff there is a second set so that both sets fulfil the wff of the class abstraction. (Contributed by AV, 19-Oct-2023.)
⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑦𝜓))
Theorem	dmopab2rex 5897*	The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.)
⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)})
Theorem	dmopabss 5898*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	dmopab3 5899*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴)
Theorem	dm0 5900	The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ dom ∅ = ∅