P. 50 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4901-5000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexxpf 4901*	Version of rexxp 4898 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	iunxpf 4902*	Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)    ⇒   ⊢ ∪ 𝑥 ∈ (𝐴 × 𝐵)𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑧 ∈ 𝐵 𝐷
Theorem	opabbi2dv 4903*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2353. (Contributed by NM, 24-Feb-2014.)
⊢ Rel 𝐴    &   ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	relop 4904*	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
Theorem	ideqg 4905	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 4906	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)
Theorem	ididg 4907	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
Theorem	issetid 4908	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 4909	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
Theorem	coss2 4910	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
Theorem	coeq1 4911	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2 4912	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq1i 4913	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)
Theorem	coeq2i 4914	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)
Theorem	coeq1d 4915	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2d 4916	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq12i 4917	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)
Theorem	coeq12d 4918	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))
Theorem	nfco 4919	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵)
Theorem	elco 4920*	Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝐴 ∈ (𝑅 ∘ 𝑆) ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑧⟩ ∧ (𝑥𝑆𝑦 ∧ 𝑦𝑅𝑧)))
Theorem	brcog 4921*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
Theorem	opelco2g 4922*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶)))
Theorem	brcogw 4923	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵)
Theorem	eqbrrdva 4924*	Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷))    &   ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	brco 4925*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	opelco 4926*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	cnvss 4927	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
Theorem	cnveq 4928	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
Theorem	cnveqi 4929	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ◡𝐴 = ◡𝐵
Theorem	cnveqd 4930	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ◡𝐴 = ◡𝐵)
Theorem	elcnv 4931*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥))
Theorem	elcnv2 4932*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
Theorem	nfcnv 4933	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥◡𝐴
Theorem	opelcnvg 4934	Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
Theorem	brcnvg 4935	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	opelcnv 4936	Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Theorem	brcnv 4937	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	csbcnvg 4938	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹)
Theorem	cnvco 4939	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 4940*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
Theorem	dfdm3 4941*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	dfrn2 4942*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	dfrn3 4943*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	elrn2g 4944*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	elrng 4945*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
Theorem	ssrelrn 4946*	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 4947	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = ran ◡𝐴
Theorem	dfdmf 4948*	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 4949	Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵)
Theorem	eldmg 4950*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Theorem	eldm2g 4951*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
Theorem	eldm 4952*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Theorem	eldm2 4953*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)
Theorem	dmss 4954	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
Theorem	dmeq 4955	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Theorem	dmeqi 4956	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ dom 𝐴 = dom 𝐵
Theorem	dmeqd 4957	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐴 = dom 𝐵)
Theorem	opeldm 4958	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)
Theorem	breldm 4959	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	opeldmg 4960	Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶))
Theorem	breldmg 4961	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	dmun 4962	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 4963	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 4964	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	dmuni 4965*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	dmopab 4966*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Theorem	dmopabss 4967*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	dmopab3 4968*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴)
Theorem	dm0 4969	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 4970	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 4971	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
⊢ dom V = V
Theorem	dm0rn0 4972	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4975. (Contributed by NM, 21-May-1998.)
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Theorem	reldm0 4973	A relation is empty iff its domain is empty. For a similar theorem for whether the relation and domain are inhabited, see reldmm 4974. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Theorem	reldmm 4974*	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
⊢ (Rel 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ dom 𝐴))
Theorem	dmmrnm 4975*	A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑦 ∈ ran 𝐴)
Theorem	dmxpm 4976*	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 4977	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
⊢ dom (𝐴 × 𝐴) = 𝐴
Theorem	dmxpin 4978	The domain of the intersection of two square Cartesian products. Unlike dmin 4963, equality holds. (Contributed by NM, 29-Jan-2008.)
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	xpid11 4979	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 4980	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5212). (Contributed by NM, 8-Apr-2007.)
⊢ dom ◡◡𝐴 = dom 𝐴
Theorem	rncnvcnv 4981	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ ran ◡◡𝐴 = ran 𝐴
Theorem	elreldm 4982	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 4983	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
Theorem	rneqi 4984	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ran 𝐴 = ran 𝐵
Theorem	rneqd 4985	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐴 = ran 𝐵)
Theorem	rnss 4986	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
Theorem	brelrng 4987	The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶)
Theorem	opelrng 4988	Membership of second member of an ordered pair in a range. (Contributed by Jim Kingdon, 26-Jan-2019.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) → 𝐵 ∈ ran 𝐶)
Theorem	brelrn 4989	The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶)
Theorem	opelrn 4990	Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶)
Theorem	releldm 4991	The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	relelrn 4992	The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅)
Theorem	releldmb 4993*	Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
Theorem	relelrnb 4994*	Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴))
Theorem	releldmi 4995	The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	relelrni 4996	The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅)
Theorem	dfrnf 4997*	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 4998*	Membership in a range. (Contributed by NM, 10-Jul-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)
Theorem	elrn 4999*	Membership in a range. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)
Theorem	nfdm 5000	Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥dom 𝐴