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	xpindi 4801	Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶))
Theorem	xpindir 4802	Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶))
Theorem	xpiindim 4803*	Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))
Theorem	xpriindim 4804*	Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)))
Theorem	eliunxp 4805*	Membership in a union of cross products. Analogue of elxp 4680 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
Theorem	opeliunxp2 4806*	Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸)    ⇒   ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))
Theorem	raliunxp 4807*	Write a double restricted quantification as one universal quantifier. In this version of ralxp 4809, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
Theorem	rexiunxp 4808*	Write a double restricted quantification as one universal quantifier. In this version of rexxp 4810, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	ralxp 4809*	Universal quantification restricted to a cross 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 4810*	Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	djussxp 4811*	Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
Theorem	ralxpf 4812*	Version of ralxp 4809 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
Theorem	rexxpf 4813*	Version of rexxp 4810 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓)
Theorem	iunxpf 4814*	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 4815*	Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2315. (Contributed by NM, 24-Feb-2014.)
⊢ Rel 𝐴    &   ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	relop 4816*	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 4817	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 4818	For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)
Theorem	ididg 4819	A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
Theorem	issetid 4820	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 4821	Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))
Theorem	coss2 4822	Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))
Theorem	coeq1 4823	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2 4824	Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq1i 4825	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)
Theorem	coeq2i 4826	Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)
Theorem	coeq1d 4827	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
Theorem	coeq2d 4828	Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
Theorem	coeq12i 4829	Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)
Theorem	coeq12d 4830	Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))
Theorem	nfco 4831	Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵)
Theorem	elco 4832*	Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝐴 ∈ (𝑅 ∘ 𝑆) ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑧⟩ ∧ (𝑥𝑆𝑦 ∧ 𝑦𝑅𝑧)))
Theorem	brcog 4833*	Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)))
Theorem	opelco2g 4834*	Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶)))
Theorem	brcogw 4835	Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵)
Theorem	eqbrrdva 4836*	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 4837*	Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	opelco 4838*	Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))
Theorem	cnvss 4839	Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
Theorem	cnveq 4840	Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
Theorem	cnveqi 4841	Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ◡𝐴 = ◡𝐵
Theorem	cnveqd 4842	Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ◡𝐴 = ◡𝐵)
Theorem	elcnv 4843*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥))
Theorem	elcnv2 4844*	Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
Theorem	nfcnv 4845	Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥◡𝐴
Theorem	opelcnvg 4846	Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
Theorem	brcnvg 4847	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	opelcnv 4848	Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Theorem	brcnv 4849	The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)
Theorem	csbcnvg 4850	Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹)
Theorem	cnvco 4851	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 4852*	The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥
Theorem	dfdm3 4853*	Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	dfrn2 4854*	Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
Theorem	dfrn3 4855*	Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
Theorem	elrn2g 4856*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵))
Theorem	elrng 4857*	Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴))
Theorem	dfdm4 4858	Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
⊢ dom 𝐴 = ran ◡𝐴
Theorem	dfdmf 4859*	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 4860	Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵)
Theorem	eldmg 4861*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Theorem	eldm2g 4862*	Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵))
Theorem	eldm 4863*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)
Theorem	eldm2 4864*	Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)
Theorem	dmss 4865	Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
Theorem	dmeq 4866	Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
Theorem	dmeqi 4867	Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ dom 𝐴 = dom 𝐵
Theorem	dmeqd 4868	Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐴 = dom 𝐵)
Theorem	opeldm 4869	Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)
Theorem	breldm 4870	Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅)
Theorem	opeldmg 4871	Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶))
Theorem	breldmg 4872	Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)
Theorem	dmun 4873	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 4874	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 4875	The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵
Theorem	dmuni 4876*	The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	dmopab 4877*	The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Theorem	dmopabss 4878*	Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴
Theorem	dmopab3 4879*	The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴)
Theorem	dm0 4880	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 4881	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 4882	The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)
⊢ dom V = V
Theorem	dm0rn0 4883	An empty domain implies an empty range. For a similar theorem for whether the domain and range are inhabited, see dmmrnm 4885. (Contributed by NM, 21-May-1998.)
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Theorem	reldm0 4884	A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅))
Theorem	dmmrnm 4885*	A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
⊢ (∃𝑥 𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑦 ∈ ran 𝐴)
Theorem	dmxpm 4886*	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 4887	The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
⊢ dom (𝐴 × 𝐴) = 𝐴
Theorem	dmxpin 4888	The domain of the intersection of two square Cartesian products. Unlike dmin 4874, equality holds. (Contributed by NM, 29-Jan-2008.)
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	xpid11 4889	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 4890	The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5120). (Contributed by NM, 8-Apr-2007.)
⊢ dom ◡◡𝐴 = dom 𝐴
Theorem	rncnvcnv 4891	The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
⊢ ran ◡◡𝐴 = ran 𝐴
Theorem	elreldm 4892	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 4893	Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
Theorem	rneqi 4894	Equality inference for range. (Contributed by NM, 4-Mar-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ran 𝐴 = ran 𝐵
Theorem	rneqd 4895	Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐴 = ran 𝐵)
Theorem	rnss 4896	Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)
Theorem	brelrng 4897	The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶)
Theorem	opelrng 4898	Membership of second member of an ordered pair in a range. (Contributed by Jim Kingdon, 26-Jan-2019.)
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) → 𝐵 ∈ ran 𝐶)
Theorem	brelrn 4899	The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶)
Theorem	opelrn 4900	Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶)