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