Home | Metamath
Proof Explorer Theorem List (p. 59 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opabbi2dv 5801* | Deduce equality of a relation and an ordered-pair class abstraction. Compare abbi2dv 2876. (Contributed by NM, 24-Feb-2014.) |
⊢ Rel 𝐴 & ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜓}) | ||
Theorem | relop 5802* | A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg 5755, as funsng 6547 is to funop 7089. (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) | ||
Theorem | ideqg 5803 | 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 5804 | For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | ididg 5805 | A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) | ||
Theorem | issetid 5806 | 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 5807 | Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | ||
Theorem | coss2 5808 | Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1 5809 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2 5810 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1i 5811 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) | ||
Theorem | coeq2i 5812 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) | ||
Theorem | coeq1d 5813 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2d 5814 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq12i 5815 | Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) | ||
Theorem | coeq12d 5816 | Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) | ||
Theorem | nfco 5817 | Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) | ||
Theorem | brcog 5818* | Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) | ||
Theorem | opelco2g 5819* | Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶))) | ||
Theorem | brcogw 5820 | Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) | ||
Theorem | eqbrrdva 5821* | Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷)) & ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | brco 5822* | Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | opelco 5823* | Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | cnvss 5824 | Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnveq 5825 | Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | ||
Theorem | cnveqi 5826 | Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 | ||
Theorem | cnveqd 5827 | Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) | ||
Theorem | elcnv 5828* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥)) | ||
Theorem | elcnv2 5829* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)) | ||
Theorem | nfcnv 5830 | Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 | ||
Theorem | brcnvg 5831 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | opelcnvg 5832 | Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)) | ||
Theorem | opelcnv 5833 | Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅) | ||
Theorem | brcnv 5834 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | csbcnv 5835 | Move class substitution in and out of the converse of a relation. Version of csbcnvgALT 5836 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹 | ||
Theorem | csbcnvgALT 5836 | Move class substitution in and out of the converse of a relation. Version of csbcnv 5835 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 5837 | 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 5838* | The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.) |
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 | ||
Theorem | dfdm3 5839* | Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴} | ||
Theorem | dfrn2 5840* | Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | ||
Theorem | dfrn3 5841* | Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴} | ||
Theorem | elrn2g 5842* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)) | ||
Theorem | elrng 5843* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) | ||
Theorem | elrn2 5844* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵) | ||
Theorem | elrn 5845* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) | ||
Theorem | ssrelrn 5846* | 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 5847 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = ran ◡𝐴 | ||
Theorem | dfdmf 5848* | 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 5849 | 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 5850* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | ||
Theorem | eldm2g 5851* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)) | ||
Theorem | eldm 5852* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) | ||
Theorem | eldm2 5853* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵) | ||
Theorem | dmss 5854 | Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) | ||
Theorem | dmeq 5855 | Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) | ||
Theorem | dmeqi 5856 | Equality inference for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 | ||
Theorem | dmeqd 5857 | Equality deduction for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) | ||
Theorem | opeldmd 5858 | Membership of first of an ordered pair in a domain. Deduction version of opeldm 5859. (Contributed by AV, 11-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) | ||
Theorem | opeldm 5859 | Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶) | ||
Theorem | breldm 5860 | Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | breldmg 5861 | Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | dmun 5862 | 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 5863 | 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 5864 | Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) | ||
Theorem | dmiun 5865 | The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵 | ||
Theorem | dmuni 5866* | The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.) |
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
Theorem | dmopab 5867* | The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} | ||
Theorem | dmopabelb 5868* | 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 5869* | The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.) |
⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)}) | ||
Theorem | dmopabss 5870* | Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | dmopab3 5871* | The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) | ||
Theorem | dm0 5872 | 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 5873 | 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 5874 | The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.) |
⊢ dom V = V | ||
Theorem | dmep 5875 | 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 5876 | An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) |
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) | ||
Theorem | rn0 5877 | 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 5878 | 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 5879 | A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) | ||
Theorem | dmxp 5880 | 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 5881 | The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995.) |
⊢ dom (𝐴 × 𝐴) = 𝐴 | ||
Theorem | dmxpin 5882 | The domain of the intersection of two Cartesian squares. Unlike in dmin 5863, equality holds. (Contributed by NM, 29-Jan-2008.) |
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) | ||
Theorem | xpid11 5883 | 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 5884 | 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 6137 gives another proof). (Contributed by NM, 8-Apr-2007.) |
⊢ dom ◡◡𝐴 = dom 𝐴 | ||
Theorem | rncnvcnv 5885 | 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 5886 | The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb 5426). (Contributed by NM, 28-Jul-2004.) |
⊢ ((Rel 𝐴 ∧ 𝐵 ∈ 𝐴) → ∩ ∩ 𝐵 ∈ dom 𝐴) | ||
Theorem | rneq 5887 | Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) | ||
Theorem | rneqi 5888 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 | ||
Theorem | rneqd 5889 | Equality deduction for range. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ran 𝐴 = ran 𝐵) | ||
Theorem | rnss 5890 | Subset theorem for range. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵) | ||
Theorem | rnssi 5891 | Subclass inference for range. (Contributed by Peter Mazsa, 24-Sep-2022.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ran 𝐴 ⊆ ran 𝐵 | ||
Theorem | brelrng 5892 | The second argument of a binary relation belongs to its range. (Contributed by NM, 29-Jun-2008.) |
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐴𝐶𝐵) → 𝐵 ∈ ran 𝐶) | ||
Theorem | brelrn 5893 | The second argument of a binary relation belongs to its range. (Contributed by NM, 13-Aug-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝐶𝐵 → 𝐵 ∈ ran 𝐶) | ||
Theorem | opelrn 5894 | Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → 𝐵 ∈ ran 𝐶) | ||
Theorem | releldm 5895 | The first argument of a binary relation belongs to its domain. Note that 𝐴𝑅𝐵 does not imply Rel 𝑅: see for example nrelv 5752 and brv 5427. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrn 5896 | The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008.) |
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ ran 𝑅) | ||
Theorem | releldmb 5897* | Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥)) | ||
Theorem | relelrnb 5898* | Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ ran 𝑅 ↔ ∃𝑥 𝑥𝑅𝐴)) | ||
Theorem | releldmi 5899 | The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | relelrni 5900 | The second argument of a binary relation belongs to its range. (Contributed by NM, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴𝑅𝐵 → 𝐵 ∈ ran 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |