Theorem List for Intuitionistic Logic Explorer - 4701-4800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | issetid 4701 |
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 4702 |
Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) |
|
Theorem | coss2 4703 |
Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1 4704 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
|
Theorem | coeq2 4705 |
Equality theorem for composition of two classes. (Contributed by NM,
3-Jan-1997.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
|
Theorem | coeq1i 4706 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) |
|
Theorem | coeq2i 4707 |
Equality inference for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) |
|
Theorem | coeq1d 4708 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) |
|
Theorem | coeq2d 4709 |
Equality deduction for composition of two classes. (Contributed by NM,
16-Nov-2000.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) |
|
Theorem | coeq12i 4710 |
Equality inference for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) |
|
Theorem | coeq12d 4711 |
Equality deduction for composition of two classes. (Contributed by FL,
7-Jun-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) |
|
Theorem | nfco 4712 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 1-Sep-1999.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) |
|
Theorem | elco 4713* |
Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
|
⊢ (𝐴 ∈ (𝑅 ∘ 𝑆) ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = 〈𝑥, 𝑧〉 ∧ (𝑥𝑆𝑦 ∧ 𝑦𝑅𝑧))) |
|
Theorem | brcog 4714* |
Ordered pair membership in a composition. (Contributed by NM,
24-Feb-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) |
|
Theorem | opelco2g 4715* |
Ordered pair membership in a composition. (Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐷 ∧ 〈𝑥, 𝐵〉 ∈ 𝐶))) |
|
Theorem | brcogw 4716 |
Ordered pair membership in a composition. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) |
|
Theorem | eqbrrdva 4717* |
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 4718* |
Binary relation on a composition. (Contributed by NM, 21-Sep-2004.)
(Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
|
Theorem | opelco 4719* |
Ordered pair membership in a composition. (Contributed by NM,
27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) |
|
Theorem | cnvss 4720 |
Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
|
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) |
|
Theorem | cnveq 4721 |
Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
|
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) |
|
Theorem | cnveqi 4722 |
Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 |
|
Theorem | cnveqd 4723 |
Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) |
|
Theorem | elcnv 4724* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 24-Mar-1998.)
|
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝑦𝑅𝑥)) |
|
Theorem | elcnv2 4725* |
Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed
by NM, 11-Aug-2004.)
|
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
|
Theorem | nfcnv 4726 |
Bound-variable hypothesis builder for converse. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 |
|
Theorem | opelcnvg 4727 |
Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) |
|
Theorem | brcnvg 4728 |
The converse of a binary relation swaps arguments. Theorem 11 of [Suppes]
p. 61. (Contributed by NM, 10-Oct-2005.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
|
Theorem | opelcnv 4729 |
Ordered-pair membership in converse. (Contributed by NM,
13-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) |
|
Theorem | brcnv 4730 |
The converse of a binary relation swaps arguments. Theorem 11 of
[Suppes] p. 61. (Contributed by NM,
13-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) |
|
Theorem | csbcnvg 4731 |
Move class substitution in and out of the converse of a function.
(Contributed by Thierry Arnoux, 8-Feb-2017.)
|
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹) |
|
Theorem | cnvco 4732 |
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 4733* |
The converse of a class union is the (indexed) union of the converses of
its members. (Contributed by NM, 11-Aug-2004.)
|
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 |
|
Theorem | dfdm3 4734* |
Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴} |
|
Theorem | dfrn2 4735* |
Alternate definition of range. Definition 4 of [Suppes] p. 60.
(Contributed by NM, 27-Dec-1996.)
|
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} |
|
Theorem | dfrn3 4736* |
Alternate definition of range. Definition 6.5(2) of [TakeutiZaring]
p. 24. (Contributed by NM, 28-Dec-1996.)
|
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} |
|
Theorem | elrn2g 4737* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵)) |
|
Theorem | elrng 4738* |
Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) |
|
Theorem | dfdm4 4739 |
Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
|
⊢ dom 𝐴 = ran ◡𝐴 |
|
Theorem | dfdmf 4740* |
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 4741 |
Distribute proper substitution through the domain of a class.
(Contributed by Jim Kingdon, 8-Dec-2018.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | eldmg 4742* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) |
|
Theorem | eldm2g 4743* |
Domain membership. Theorem 4 of [Suppes] p. 59.
(Contributed by NM,
27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) |
|
Theorem | eldm 4744* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 2-Apr-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
|
Theorem | eldm2 4745* |
Membership in a domain. Theorem 4 of [Suppes]
p. 59. (Contributed by
NM, 1-Aug-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
|
Theorem | dmss 4746 |
Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) |
|
Theorem | dmeq 4747 |
Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
|
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) |
|
Theorem | dmeqi 4748 |
Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 |
|
Theorem | dmeqd 4749 |
Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) |
|
Theorem | opeldm 4750 |
Membership of first of an ordered pair in a domain. (Contributed by NM,
30-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶) |
|
Theorem | breldm 4751 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 30-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
|
Theorem | opeldmg 4752 |
Membership of first of an ordered pair in a domain. (Contributed by Jim
Kingdon, 9-Jul-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) |
|
Theorem | breldmg 4753 |
Membership of first of a binary relation in a domain. (Contributed by
NM, 21-Mar-2007.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
|
Theorem | dmun 4754 |
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 4755 |
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 4756 |
The domain of an indexed union. (Contributed by Mario Carneiro,
26-Apr-2016.)
|
⊢ dom ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 dom 𝐵 |
|
Theorem | dmuni 4757* |
The domain of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 3-Feb-2004.)
|
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 |
|
Theorem | dmopab 4758* |
The domain of a class of ordered pairs. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ dom {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} |
|
Theorem | dmopabss 4759* |
Upper bound for the domain of a restricted class of ordered pairs.
(Contributed by NM, 31-Jan-2004.)
|
⊢ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 |
|
Theorem | dmopab3 4760* |
The domain of a restricted class of ordered pairs. (Contributed by NM,
31-Jan-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) |
|
Theorem | dm0 4761 |
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 4762 |
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 4763 |
The domain of the universe is the universe. (Contributed by NM,
8-Aug-2003.)
|
⊢ dom V = V |
|
Theorem | dm0rn0 4764 |
An empty domain implies an empty range. For a similar theorem for
whether the domain and range are inhabited, see dmmrnm 4766. (Contributed
by NM, 21-May-1998.)
|
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) |
|
Theorem | reldm0 4765 |
A relation is empty iff its domain is empty. (Contributed by NM,
15-Sep-2004.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) |
|
Theorem | dmmrnm 4766* |
A domain is inhabited if and only if the range is inhabited.
(Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑦 ∈ ran 𝐴) |
|
Theorem | dmxpm 4767* |
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 4768 |
The domain of a square Cartesian product. (Contributed by NM,
28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.)
|
⊢ dom (𝐴 × 𝐴) = 𝐴 |
|
Theorem | dmxpin 4769 |
The domain of the intersection of two square Cartesian products. Unlike
dmin 4755, equality holds. (Contributed by NM,
29-Jan-2008.)
|
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) |
|
Theorem | xpid11 4770 |
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 4771 |
The domain of the double converse of a class (which doesn't have to be a
relation as in dfrel2 4997). (Contributed by NM, 8-Apr-2007.)
|
⊢ dom ◡◡𝐴 = dom 𝐴 |
|
Theorem | rncnvcnv 4772 |
The range of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
⊢ ran ◡◡𝐴 = ran 𝐴 |
|
Theorem | elreldm 4773 |
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 4774 |
Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
|
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) |
|
Theorem | rneqi 4775 |
Equality inference for range. (Contributed by NM, 4-Mar-2004.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 |
|
Theorem | rneqd 4776 |
Equality deduction for range. (Contributed by NM, 4-Mar-2004.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ran 𝐴 = ran 𝐵) |
|
Theorem | rnss 4777 |
Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
|
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) |
|
Theorem | brelrng 4778 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 29-Jun-2008.)
|
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶) |
|
Theorem | opelrng 4779 |
Membership of second member of an ordered pair in a range. (Contributed
by Jim Kingdon, 26-Jan-2019.)
|
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) → 𝐵 ∈ ran 𝐶) |
|
Theorem | brelrn 4780 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 13-Aug-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶) |
|
Theorem | opelrn 4781 |
Membership of second member of an ordered pair in a range. (Contributed
by NM, 23-Feb-1997.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐵 ∈ ran 𝐶) |
|
Theorem | releldm 4782 |
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 2-Jul-2008.)
|
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) |
|
Theorem | relelrn 4783 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 2-Jul-2008.)
|
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅) |
|
Theorem | releldmb 4784* |
Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥)) |
|
Theorem | relelrnb 4785* |
Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴)) |
|
Theorem | releldmi 4786 |
The first argument of a binary relation belongs to its domain.
(Contributed by NM, 28-Apr-2015.)
|
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) |
|
Theorem | relelrni 4787 |
The second argument of a binary relation belongs to its range.
(Contributed by NM, 28-Apr-2015.)
|
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅) |
|
Theorem | dfrnf 4788* |
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 4789* |
Membership in a range. (Contributed by NM, 10-Jul-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵) |
|
Theorem | elrn 4790* |
Membership in a range. (Contributed by NM, 2-Apr-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) |
|
Theorem | nfdm 4791 |
Bound-variable hypothesis builder for domain. (Contributed by NM,
30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥dom 𝐴 |
|
Theorem | nfrn 4792 |
Bound-variable hypothesis builder for range. (Contributed by NM,
1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥ran 𝐴 |
|
Theorem | dmiin 4793 |
Domain of an intersection. (Contributed by FL, 15-Oct-2012.)
|
⊢ dom ∩
𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵 |
|
Theorem | rnopab 4794* |
The range of a class of ordered pairs. (Contributed by NM,
14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ ran {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑} |
|
Theorem | rnmpt 4795* |
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 4796* |
The range of a function in maps-to notation. (Contributed by Mario
Carneiro, 20-Feb-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) |
|
Theorem | elrnmpt1s 4797* |
Elementhood in an image set. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
|
Theorem | elrnmpt1 4798 |
Elementhood in an image set. (Contributed by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) |
|
Theorem | elrnmptg 4799* |
Membership in the range of a function. (Contributed by NM,
27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) |
|
Theorem | elrnmpti 4800* |
Membership in the range of a function. (Contributed by NM,
30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |