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	ideqg 5801	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 5802	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)
Theorem	ididg 5803	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
Theorem	issetid 5804	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 5805	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
Theorem	coss2 5806	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
Theorem	coeq1 5807	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2 5808	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq1i 5809	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)
Theorem	coeq2i 5810	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)
Theorem	coeq1d 5811	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2d 5812	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq12i 5813	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)
Theorem	coeq12d 5814	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))
Theorem	nfco 5815	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵)
Theorem	brcog 5816*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
Theorem	opelco2g 5817*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶)))
Theorem	brcogw 5818	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵)
Theorem	eqbrrdva 5819*	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 5820*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	opelco 5821*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	cnvss 5822	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.)
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
Theorem	cnveq 5823	Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.)
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
Theorem	cnveqi 5824	Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ◡𝐴 = ◡𝐵
Theorem	cnveqd 5825	Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ◡𝐴 = ◡𝐵)
Theorem	elcnv 5826*	Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥))
Theorem	elcnv2 5827*	Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
Theorem	nfcnv 5828	Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥◡𝐴
Theorem	brcnvg 5829	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	opelcnvg 5830	Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
Theorem	opelcnv 5831	Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Theorem	brcnv 5832	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	csbcnv 5833	Move class substitution in and out of the converse of a relation. Version of csbcnvgALT 5834 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.)
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹
Theorem	csbcnvgALT 5834	Move class substitution in and out of the converse of a relation. Version of csbcnv 5833 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 5835	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 5836*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
Theorem	dfdm3 5837*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	dfrn2 5838*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	dfrn3 5839*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	elrn2g 5840*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	elrng 5841*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
Theorem	elrn2 5842*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)
Theorem	elrn 5843*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)
Theorem	ssrelrn 5844*	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 5845	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = ran ◡𝐴
Theorem	dfdmf 5846*	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 5847	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 5848*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Theorem	eldm2g 5849*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
Theorem	eldm 5850*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Theorem	eldm2 5851*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)
Theorem	dmss 5852	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
Theorem	dmeq 5853	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Theorem	dmeqi 5854	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ dom 𝐴 = dom 𝐵
Theorem	dmeqd 5855	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐴 = dom 𝐵)
Theorem	opeldmd 5856	Membership of first of an ordered pair in a domain. Deduction version of opeldm 5857. (Contributed by AV, 11-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶))
Theorem	opeldm 5857	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)
Theorem	breldm 5858	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	breldmg 5859	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	dmun 5860	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 5861	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 5862	Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
Theorem	dmiun 5863	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	dmuni 5864*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	dmopab 5865*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Theorem	dmopabelb 5866*	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 5867*	The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.)
⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)})
Theorem	dmopabss 5868*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	dmopab3 5869*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴)
Theorem	dm0 5870	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 ∅ = ∅
Theorem	dmi 5871	The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ dom I = V
Theorem	dmv 5872	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
⊢ dom V = V
Theorem	dmep 5873	The domain of the membership relation is the universal class. (Contributed by Scott Fenton, 27-Oct-2010.) (Proof shortened by BJ, 26-Dec-2023.)
⊢ dom E = V
Theorem	dm0rn0 5874	An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (Revised by TM, 24-Jan-2026.)
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Theorem	dm0rn0OLD 5875	Obsolete version of dm0rn0 5874 as of 24-Jan-2026. (Contributed by NM, 21-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Theorem	rn0 5876	The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.)
⊢ ran ∅ = ∅
Theorem	rnep 5877	The range of the membership relation is the universal class minus the empty set. (Contributed by BJ, 26-Dec-2023.)
⊢ ran E = (V ∖ {∅})
Theorem	reldm0 5878	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Theorem	dmxp 5879	The domain of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (Revised by SN, 12-Aug-2025.)
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Theorem	dmxpid 5880	The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995.)
⊢ dom (𝐴 × 𝐴) = 𝐴
Theorem	dmxpin 5881	The domain of the intersection of two Cartesian squares. Unlike in dmin 5861, equality holds. (Contributed by NM, 29-Jan-2008.)
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	xpid11 5882	The Cartesian square is a one-to-one construction. (Contributed by NM, 5-Nov-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 × 𝐴) = (𝐵 × 𝐵) ↔ 𝐴 = 𝐵)
Theorem	dmcnvcnv 5883	The domain of the double converse of a class is equal to its domain (even when that class in not a relation, in which case dfrel2 6148 gives another proof). (Contributed by NM, 8-Apr-2007.)
⊢ dom ◡◡𝐴 = dom 𝐴
Theorem	rncnvcnv 5884	The range of the double converse of a class is equal to its range (even when that class in not a relation). (Contributed by NM, 8-Apr-2007.)
⊢ ran ◡◡𝐴 = ran 𝐴
Theorem	elreldm 5885	The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb 5420). (Contributed by NM, 28-Jul-2004.)
⊢ ((Rel 𝐴 ∧ 𝐵 ∈ 𝐴) → ∩ ∩ 𝐵 ∈ dom 𝐴)
Theorem	rneq 5886	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
Theorem	rneqi 5887	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ran 𝐴 = ran 𝐵
Theorem	rneqd 5888	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐴 = ran 𝐵)
Theorem	rnss 5889	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
Theorem	rnssi 5890	Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ran 𝐴 ⊆ ran 𝐵
Theorem	brelrng 5891	The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶)
Theorem	brelrn 5892	The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶)
Theorem	opelrn 5893	Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶)
Theorem	releldm 5894	The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5750 and brv 5421. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	relelrn 5895	The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅)
Theorem	releldmb 5896*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
Theorem	relelrnb 5897*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴))
Theorem	releldmi 5898	The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	relelrni 5899	The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅)
Theorem	dfrnf 5900*	Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}