| Metamath
Proof Explorer Theorem List (p. 60 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elrn2g 5901* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵)) | ||
| Theorem | elrng 5902* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) | ||
| Theorem | elrn2 5903* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵) | ||
| Theorem | elrn 5904* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) | ||
| Theorem | ssrelrn 5905* | 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 5906 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
| ⊢ dom 𝐴 = ran ◡𝐴 | ||
| Theorem | dfdmf 5907* | 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 5908 | 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 5909* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | ||
| Theorem | eldm2g 5910* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | ||
| Theorem | eldm 5911* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) | ||
| Theorem | eldm2 5912* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) | ||
| Theorem | dmss 5913 | Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) | ||
| Theorem | dmeq 5914 | Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
| ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) | ||
| Theorem | dmeqi 5915 | Equality inference for domain. (Contributed by NM, 4-Mar-2004.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 | ||
| Theorem | dmeqd 5916 | Equality deduction for domain. (Contributed by NM, 4-Mar-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) | ||
| Theorem | opeldmd 5917 | Membership of first of an ordered pair in a domain. Deduction version of opeldm 5918. (Contributed by AV, 11-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) | ||
| Theorem | opeldm 5918 | Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶) | ||
| Theorem | breldm 5919 | Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
| Theorem | breldmg 5920 | Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
| Theorem | dmun 5921 | 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 5922 | 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 5923 | Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) | ||
| Theorem | dmiun 5924 | The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵 | ||
| Theorem | dmuni 5925* | The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.) |
| ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
| Theorem | dmopab 5926* | The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
| ⊢ dom {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} | ||
| Theorem | dmopabelb 5927* | A set is an element of the domain of a 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 5928* | The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.) |
| ⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)}) | ||
| Theorem | dmopabss 5929* | Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
| ⊢ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
| Theorem | dmopab3 5930* | The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) | ||
| Theorem | dm0 5931 | 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 5932 | 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 5933 | The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.) |
| ⊢ dom V = V | ||
| Theorem | dmep 5934 | 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 5935 | An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) |
| ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) | ||
| Theorem | rn0 5936 | 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 5937 | 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 5938 | A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
| ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) | ||
| Theorem | dmxp 5939 | 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 2141, ax-11 2157, ax-12 2177. (Revised by SN, 12-Aug-2025.) |
| ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | ||
| Theorem | dmxpOLD 5940 | Obsolete version of dmxp 5939 as of 19-Dec-2024. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | ||
| Theorem | dmxpid 5941 | The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995.) |
| ⊢ dom (𝐴 × 𝐴) = 𝐴 | ||
| Theorem | dmxpin 5942 | The domain of the intersection of two Cartesian squares. Unlike in dmin 5922, equality holds. (Contributed by NM, 29-Jan-2008.) |
| ⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) | ||
| Theorem | xpid11 5943 | 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 5944 | 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 6209 gives another proof). (Contributed by NM, 8-Apr-2007.) |
| ⊢ dom ◡◡𝐴 = dom 𝐴 | ||
| Theorem | rncnvcnv 5945 | 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 5946 | The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb 5476). (Contributed by NM, 28-Jul-2004.) |
| ⊢ ((Rel 𝐴 ∧ 𝐵 ∈ 𝐴) → ∩ ∩ 𝐵 ∈ dom 𝐴) | ||
| Theorem | rneq 5947 | Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
| ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) | ||
| Theorem | rneqi 5948 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 | ||
| Theorem | rneqd 5949 | Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ran 𝐴 = ran 𝐵) | ||
| Theorem | rnss 5950 | Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
| ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) | ||
| Theorem | rnssi 5951 | Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.) |
| ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ran 𝐴 ⊆ ran 𝐵 | ||
| Theorem | brelrng 5952 | The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.) |
| ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶) | ||
| Theorem | brelrn 5953 | The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶) | ||
| Theorem | opelrn 5954 | Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐵 ∈ ran 𝐶) | ||
| Theorem | releldm 5955 | The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5810 and brv 5477. (Contributed by NM, 2-Jul-2008.) |
| ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
| Theorem | relelrn 5956 | The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.) |
| ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅) | ||
| Theorem | releldmb 5957* | Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.) |
| ⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥)) | ||
| Theorem | relelrnb 5958* | Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.) |
| ⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴)) | ||
| Theorem | releldmi 5959 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
| ⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
| Theorem | relelrni 5960 | The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.) |
| ⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅) | ||
| Theorem | dfrnf 5961* | 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 5962 | Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥dom 𝐴 | ||
| Theorem | nfrn 5963 | Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥ran 𝐴 | ||
| Theorem | dmiin 5964 | Domain of an intersection. (Contributed by FL, 15-Oct-2012.) |
| ⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵 | ||
| Theorem | rnopab 5965* | The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
| ⊢ ran {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑} | ||
| Theorem | rnopabss 5966* | Upper bound for the range of a restricted class of ordered pairs. (Contributed by Eric Schmidt, 16-Sep-2025.) |
| ⊢ ran {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
| Theorem | rnopab3 5967* | The range of a restricted class of ordered pairs. (Contributed by Eric Schmidt, 16-Sep-2025.) |
| ⊢ (∀𝑦 ∈ 𝐴 ∃𝑥𝜑 ↔ ran {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} = 𝐴) | ||
| Theorem | rnmpt 5968* | 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 5969* | The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
| Theorem | elrnmpt1s 5970* | Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) | ||
| Theorem | elrnmpt1 5971 | Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) | ||
| Theorem | elrnmptg 5972* | Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
| Theorem | elrnmpti 5973* | Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) | ||
| Theorem | elrnmptd 5974* | The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran 𝐹) | ||
| Theorem | elrnmpt1d 5975 | Elementhood in an image set. Deducion version of elrnmpt1 5971. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐹) | ||
| Theorem | elrnmptdv 5976* | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
| Theorem | elrnmpt2d 5977* | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) | ||
| Theorem | dfiun3g 5978 | Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
| Theorem | dfiin3g 5979 | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
| Theorem | dfiun3 5980 | Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
| Theorem | dfiin3 5981 | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
| Theorem | riinint 5982* | Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋) → (𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆) = ∩ ({𝑋} ∪ ran (𝑘 ∈ 𝐼 ↦ 𝑆))) | ||
| Theorem | relrn0 5983 | A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004.) |
| ⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ran 𝐴 = ∅)) | ||
| Theorem | dmrnssfld 5984 | The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008.) |
| ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | ||
| Theorem | dmcoss 5985 | 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 5986 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
| ⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴 | ||
| Theorem | dmcosseq 5987 | Domain of a composition. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-11 2157. (Revised by BTernaryTau, 23-Jun-2025.) |
| ⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵) | ||
| Theorem | dmcosseqOLD 5988 | Obsolete version of dmcosseq 5987 as of 23-Jun-2025. (Contributed by NM, 28-May-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (ran 𝐵 ⊆ dom 𝐴 → dom (𝐴 ∘ 𝐵) = dom 𝐵) | ||
| Theorem | dmcoeq 5989 | Domain of a composition. (Contributed by NM, 19-Mar-1998.) |
| ⊢ (dom 𝐴 = ran 𝐵 → dom (𝐴 ∘ 𝐵) = dom 𝐵) | ||
| Theorem | rncoeq 5990 | Range of a composition. (Contributed by NM, 19-Mar-1998.) |
| ⊢ (dom 𝐴 = ran 𝐵 → ran (𝐴 ∘ 𝐵) = ran 𝐴) | ||
| Theorem | reseq1 5991 | Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | ||
| Theorem | reseq2 5992 | Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | ||
| Theorem | reseq1i 5993 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶) | ||
| Theorem | reseq2i 5994 | Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵) | ||
| Theorem | reseq12i 5995 | Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷) | ||
| Theorem | reseq1d 5996 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)) | ||
| Theorem | reseq2d 5997 | Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)) | ||
| Theorem | reseq12d 5998 | Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷)) | ||
| Theorem | nfres 5999 | Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003.) (Revised by David Abernethy, 19-Jun-2012.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ↾ 𝐵) | ||
| Theorem | csbres 6000 | Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.) |
| ⊢ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |