P. 49 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opelco 4801*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	cnvss 4802	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
Theorem	cnveq 4803	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
Theorem	cnveqi 4804	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ◡𝐴 = ◡𝐵
Theorem	cnveqd 4805	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ◡𝐴 = ◡𝐵)
Theorem	elcnv 4806*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥))
Theorem	elcnv2 4807*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
Theorem	nfcnv 4808	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥◡𝐴
Theorem	opelcnvg 4809	Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
Theorem	brcnvg 4810	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	opelcnv 4811	Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Theorem	brcnv 4812	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	csbcnvg 4813	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹)
Theorem	cnvco 4814	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 4815*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
Theorem	dfdm3 4816*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	dfrn2 4817*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	dfrn3 4818*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	elrn2g 4819*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	elrng 4820*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
Theorem	dfdm4 4821	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = ran ◡𝐴
Theorem	dfdmf 4822*	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	csbdmg 4823	Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵)
Theorem	eldmg 4824*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Theorem	eldm2g 4825*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
Theorem	eldm 4826*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Theorem	eldm2 4827*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)
Theorem	dmss 4828	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
Theorem	dmeq 4829	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Theorem	dmeqi 4830	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ dom 𝐴 = dom 𝐵
Theorem	dmeqd 4831	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐴 = dom 𝐵)
Theorem	opeldm 4832	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)
Theorem	breldm 4833	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	opeldmg 4834	Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶))
Theorem	breldmg 4835	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	dmun 4836	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 4837	The domain of an intersection belong to the intersection of domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
⊢ dom (𝐴 ∩ 𝐵) ⊆ (dom 𝐴 ∩ dom 𝐵)
Theorem	dmiun 4838	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	dmuni 4839*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	dmopab 4840*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Theorem	dmopabss 4841*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	dmopab3 4842*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴)
Theorem	dm0 4843	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 4844	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 4845	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
⊢ dom V = V
Theorem	dm0rn0 4846	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4848. (Contributed by NM, 21-May-1998.)
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Theorem	reldm0 4847	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Theorem	dmmrnm 4848*	A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑦 ∈ ran 𝐴)
Theorem	dmxpm 4849*	The domain of a cross 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.)
⊢ (∃𝑥 𝑥 ∈ 𝐵 → dom (𝐴 × 𝐵) = 𝐴)
Theorem	dmxpid 4850	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
⊢ dom (𝐴 × 𝐴) = 𝐴
Theorem	dmxpin 4851	The domain of the intersection of two square Cartesian products. Unlike dmin 4837, equality holds. (Contributed by NM, 29-Jan-2008.)
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	xpid11 4852	The Cartesian product of a class with itself is one-to-one. (Contributed by NM, 5-Nov-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 × 𝐴) = (𝐵 × 𝐵) ↔ 𝐴 = 𝐵)
Theorem	dmcnvcnv 4853	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5081). (Contributed by NM, 8-Apr-2007.)
⊢ dom ◡◡𝐴 = dom 𝐴
Theorem	rncnvcnv 4854	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ ran ◡◡𝐴 = ran 𝐴
Theorem	elreldm 4855	The first member of an ordered pair in a relation belongs to the domain of the relation. (Contributed by NM, 28-Jul-2004.)
⊢ ((Rel 𝐴 ∧ 𝐵 ∈ 𝐴) → ∩ ∩ 𝐵 ∈ dom 𝐴)
Theorem	rneq 4856	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
Theorem	rneqi 4857	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ran 𝐴 = ran 𝐵
Theorem	rneqd 4858	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐴 = ran 𝐵)
Theorem	rnss 4859	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
Theorem	brelrng 4860	The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶)
Theorem	opelrng 4861	Membership of second member of an ordered pair in a range. (Contributed by Jim Kingdon, 26-Jan-2019.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) → 𝐵 ∈ ran 𝐶)
Theorem	brelrn 4862	The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶)
Theorem	opelrn 4863	Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶)
Theorem	releldm 4864	The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	relelrn 4865	The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅)
Theorem	releldmb 4866*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
Theorem	relelrnb 4867*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴))
Theorem	releldmi 4868	The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	relelrni 4869	The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅)
Theorem	dfrnf 4870*	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	elrn2 4871*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)
Theorem	elrn 4872*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)
Theorem	nfdm 4873	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥dom 𝐴
Theorem	nfrn 4874	Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥ran 𝐴
Theorem	dmiin 4875	Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	rnopab 4876*	The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑}
Theorem	rnmpt 4877*	The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
Theorem	elrnmpt 4878*	The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	elrnmpt1s 4879*	Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)
Theorem	elrnmpt1 4880	Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹)
Theorem	elrnmptg 4881*	Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	elrnmpti 4882*	Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
Theorem	elrnmptdv 4883*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ∈ ran 𝐹)
Theorem	elrnmpt2d 4884*	Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
Theorem	rn0 4885	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	dfiun3g 4886	Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfiin3g 4887	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfiun3 4888	Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	dfiin3 4889	Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	riinint 4890*	Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋) → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) = ∩ ({𝑋} ∪ ran (𝑘 ∈ 𝐼 ↦ 𝑆)))
Theorem	relrn0 4891	A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ran 𝐴 = ∅))
Theorem	dmrnssfld 4892	The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.)
⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
Theorem	dmexg 4893	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
Theorem	rnexg 4894	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)
⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
Theorem	dmex 4895	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ dom 𝐴 ∈ V
Theorem	rnex 4896	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran 𝐴 ∈ V
Theorem	iprc 4897	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	dmcoss 4898	Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵
Theorem	rncoss 4899	Range of a composition. (Contributed by NM, 19-Mar-1998.)
⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴
Theorem	dmcosseq 4900	Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵)