Home | Metamath
Proof Explorer Theorem List (p. 53 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coeq1 5201 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2 5202 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1i 5203 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) | ||
Theorem | coeq2i 5204 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) | ||
Theorem | coeq1d 5205 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2d 5206 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq12i 5207 | Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) | ||
Theorem | coeq12d 5208 | Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) | ||
Theorem | nfco 5209 | Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) | ||
Theorem | brcog 5210* | Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) | ||
Theorem | opelco2g 5211* | Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐷 ∧ 〈𝑥, 𝐵〉 ∈ 𝐶))) | ||
Theorem | brcogw 5212 | Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) | ||
Theorem | eqbrrdva 5213* | 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 5214* | Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | opelco 5215* | Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | cnvss 5216 | Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnvssOLD 5217 | Obsolete proof of cnvss 5216 as of 27-Apr-2021. Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnveq 5218 | Equality theorem for converse. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | ||
Theorem | cnveqi 5219 | Equality inference for converse. (Contributed by NM, 23-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 | ||
Theorem | cnveqd 5220 | Equality deduction for converse. (Contributed by NM, 6-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) | ||
Theorem | elcnv 5221* | Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝑦𝑅𝑥)) | ||
Theorem | elcnv2 5222* | Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) | ||
Theorem | nfcnv 5223 | Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 | ||
Theorem | opelcnvg 5224 | Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) | ||
Theorem | brcnvg 5225 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | opelcnv 5226 | Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) | ||
Theorem | brcnv 5227 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | csbcnv 5228 | Move class substitution in and out of the converse of a function. Version of csbcnvgALT 5229 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹 | ||
Theorem | csbcnvgALT 5229 | Move class substitution in and out of the converse of a function. Version of csbcnv 5228 with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹) | ||
Theorem | cnvco 5230 | 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 5231* | The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.) |
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 | ||
Theorem | dfdm3 5232* | Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴} | ||
Theorem | dfrn2 5233* | Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | ||
Theorem | dfrn3 5234* | Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} | ||
Theorem | elrn2g 5235* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵)) | ||
Theorem | elrng 5236* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) | ||
Theorem | ssrelrn 5237* | 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 5238 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = ran ◡𝐴 | ||
Theorem | dfdmf 5239* | 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 5240 | 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 5241* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | ||
Theorem | eldm2g 5242* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | ||
Theorem | eldm 5243* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) | ||
Theorem | eldm2 5244* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) | ||
Theorem | dmss 5245 | Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) | ||
Theorem | dmeq 5246 | Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) | ||
Theorem | dmeqi 5247 | Equality inference for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 | ||
Theorem | dmeqd 5248 | Equality deduction for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) | ||
Theorem | opeldmd 5249 | Membership of first of an ordered pair in a domain. Deduction version of opeldm 5250. (Contributed by AV, 11-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) | ||
Theorem | opeldm 5250 | Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶) | ||
Theorem | breldm 5251 | Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | breldmg 5252 | Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | dmun 5253 | 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 5254 | 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 5255 | The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵 | ||
Theorem | dmuni 5256* | The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.) |
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
Theorem | dmopab 5257* | The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ dom {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} | ||
Theorem | dmopabss 5258* | Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | dmopab3 5259* | The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) | ||
Theorem | dm0 5260 | 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 5261 | 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 5262 | The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.) |
⊢ dom V = V | ||
Theorem | dm0rn0 5263 | An empty domain implies an empty range. (Contributed by NM, 21-May-1998.) |
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) | ||
Theorem | reldm0 5264 | A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) | ||
Theorem | dmxp 5265 | 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.) |
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) | ||
Theorem | dmxpid 5266 | The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) |
⊢ dom (𝐴 × 𝐴) = 𝐴 | ||
Theorem | dmxpin 5267 | The domain of the intersection of two square Cartesian products. Unlike dmin 5254, equality holds. (Contributed by NM, 29-Jan-2008.) |
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) | ||
Theorem | xpid11 5268 | 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 5269 | The domain of the double converse of a class (which doesn't have to be a relation as in dfrel2 5502). (Contributed by NM, 8-Apr-2007.) |
⊢ dom ◡◡𝐴 = dom 𝐴 | ||
Theorem | rncnvcnv 5270 | The range of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
⊢ ran ◡◡𝐴 = ran 𝐴 | ||
Theorem | elreldm 5271 | 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 5272 | Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) | ||
Theorem | rneqi 5273 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 | ||
Theorem | rneqd 5274 | Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ran 𝐴 = ran 𝐵) | ||
Theorem | rnss 5275 | Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) | ||
Theorem | brelrng 5276 | The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.) |
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶) | ||
Theorem | brelrn 5277 | The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶) | ||
Theorem | opelrn 5278 | Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐵 ∈ ran 𝐶) | ||
Theorem | releldm 5279 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrn 5280 | The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅) | ||
Theorem | releldmb 5281* | Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥)) | ||
Theorem | relelrnb 5282* | Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴)) | ||
Theorem | releldmi 5283 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrni 5284 | The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅) | ||
Theorem | dfrnf 5285* | 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 5286* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵) | ||
Theorem | elrn 5287* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) | ||
Theorem | nfdm 5288 | Bound-variable hypothesis builder for domain. (Contributed by NM, 30-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥dom 𝐴 | ||
Theorem | nfrn 5289 | Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥ran 𝐴 | ||
Theorem | dmiin 5290 | Domain of an intersection. (Contributed by FL, 15-Oct-2012.) |
⊢ dom ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 dom 𝐵 | ||
Theorem | rnopab 5291* | The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ ran {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑} | ||
Theorem | rnmpt 5292* | 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 5293* | The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
Theorem | elrnmpt1s 5294* | Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) | ||
Theorem | elrnmpt1 5295 | Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) | ||
Theorem | elrnmptg 5296* | Membership in the range of a function. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
Theorem | elrnmpti 5297* | Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) | ||
Theorem | rn0 5298 | 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 5299 | Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | dfiin3g 5300 | Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |