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