Home | Metamath
Proof Explorer Theorem List (p. 58 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eliunxp 5701* | Membership in a union of Cartesian products. Analogue of elxp 5571 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | opeliunxp2 5702* | Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | raliunxp 5703* | Write a double restricted quantification as one universal quantifier. In this version of ralxp 5705, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexiunxp 5704* | Write a double restricted quantification as one universal quantifier. In this version of rexxp 5706, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | ralxp 5705* | Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxp 5706* | Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | exopxfr 5707* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (V × V)𝜑 ↔ ∃𝑦∃𝑧𝜓) | ||
Theorem | exopxfr2 5708* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) |
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (Rel 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑧(〈𝑦, 𝑧〉 ∈ 𝐴 ∧ 𝜓))) | ||
Theorem | djussxp 5709* | Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) | ||
Theorem | ralxpf 5710* | Version of ralxp 5705 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxpf 5711* | Version of rexxp 5706 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | iunxpf 5712* | 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 5713* | Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2947. (Contributed by NM, 24-Feb-2014.) |
⊢ Rel 𝐴 & ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | relop 5714* | A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. Compare with relsnopg 5669. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (Rel 〈𝐴, 𝐵〉 ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) | ||
Theorem | ideqg 5715 | 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 5716 | For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | ididg 5717 | A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) | ||
Theorem | issetid 5718 | 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 5719 | Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | ||
Theorem | coss2 5720 | Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1 5721 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2 5722 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1i 5723 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) | ||
Theorem | coeq2i 5724 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) | ||
Theorem | coeq1d 5725 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2d 5726 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq12i 5727 | Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) | ||
Theorem | coeq12d 5728 | Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) | ||
Theorem | nfco 5729 | Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) | ||
Theorem | brcog 5730* | Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) | ||
Theorem | opelco2g 5731* | Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐷 ∧ 〈𝑥, 𝐵〉 ∈ 𝐶))) | ||
Theorem | brcogw 5732 | Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) | ||
Theorem | eqbrrdva 5733* | 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 5734* | Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | opelco 5735* | Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | cnvss 5736 | Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnveq 5737 | Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | ||
Theorem | cnveqi 5738 | Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 | ||
Theorem | cnveqd 5739 | Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) | ||
Theorem | elcnv 5740* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝑦𝑅𝑥)) | ||
Theorem | elcnv2 5741* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) | ||
Theorem | nfcnv 5742 | Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 | ||
Theorem | brcnvg 5743 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | opelcnvg 5744 | Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) | ||
Theorem | opelcnv 5745 | Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) | ||
Theorem | brcnv 5746 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | csbcnv 5747 | Move class substitution in and out of the converse of a relation. Version of csbcnvgALT 5748 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹 | ||
Theorem | csbcnvgALT 5748 | Move class substitution in and out of the converse of a relation. Version of csbcnv 5747 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 5749 | 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 5750* | The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.) |
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 | ||
Theorem | dfdm3 5751* | Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴} | ||
Theorem | dfrn2 5752* | Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | ||
Theorem | dfrn3 5753* | Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐴} | ||
Theorem | elrn2g 5754* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥〈𝑥, 𝐴〉 ∈ 𝐵)) | ||
Theorem | elrng 5755* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) | ||
Theorem | ssrelrn 5756* | 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 5757 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = ran ◡𝐴 | ||
Theorem | dfdmf 5758* | 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 5759 | 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 5760* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | ||
Theorem | eldm2g 5761* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | ||
Theorem | eldm 5762* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) | ||
Theorem | eldm2 5763* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) | ||
Theorem | dmss 5764 | Subset theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) | ||
Theorem | dmeq 5765 | Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) | ||
Theorem | dmeqi 5766 | Equality inference for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ dom 𝐴 = dom 𝐵 | ||
Theorem | dmeqd 5767 | Equality deduction for domain. (Contributed by NM, 4-Mar-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → dom 𝐴 = dom 𝐵) | ||
Theorem | opeldmd 5768 | Membership of first of an ordered pair in a domain. Deduction version of opeldm 5769. (Contributed by AV, 11-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶)) | ||
Theorem | opeldm 5769 | Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → 𝐴 ∈ dom 𝐶) | ||
Theorem | breldm 5770 | Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ dom 𝑅) | ||
Theorem | breldmg 5771 | Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅) | ||
Theorem | dmun 5772 | 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 5773 | 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 5774 | Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) | ||
Theorem | dmiun 5775 | The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵 | ||
Theorem | dmuni 5776* | The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.) |
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 | ||
Theorem | dmopab 5777* | The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ dom {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑} | ||
Theorem | dmopabelb 5778* | 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 5779* | The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.) |
⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)}) | ||
Theorem | dmopabss 5780* | Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐴 | ||
Theorem | dmopab3 5781* | The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = 𝐴) | ||
Theorem | opabssxpd 5782* | An ordered-pair class abstraction is a subset of a Cartesian product. Formerly part of proof for opabex2 7744. (Contributed by AV, 26-Nov-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ (𝐴 × 𝐵)) | ||
Theorem | dm0 5783 | 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 5784 | 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 5785 | The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.) |
⊢ dom V = V | ||
Theorem | dmep 5786 | 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 | domepOLD 5787 | Obsolete proof of dmep 5786 as of 26-Dec-2023. (Contributed by Scott Fenton, 27-Oct-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ dom E = V | ||
Theorem | dm0rn0 5788 | An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) |
⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅) | ||
Theorem | rn0 5789 | 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 5790 | 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 5791 | A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ dom 𝐴 = ∅)) | ||
Theorem | dmxp 5792 | 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 5793 | The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995.) |
⊢ dom (𝐴 × 𝐴) = 𝐴 | ||
Theorem | dmxpin 5794 | The domain of the intersection of two Cartesian squares. Unlike in dmin 5773, equality holds. (Contributed by NM, 29-Jan-2008.) |
⊢ dom ((𝐴 × 𝐴) ∩ (𝐵 × 𝐵)) = (𝐴 ∩ 𝐵) | ||
Theorem | xpid11 5795 | 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 5796 | 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 6039 gives another proof). (Contributed by NM, 8-Apr-2007.) |
⊢ dom ◡◡𝐴 = dom 𝐴 | ||
Theorem | rncnvcnv 5797 | 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 5798 | The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb 5354). (Contributed by NM, 28-Jul-2004.) |
⊢ ((Rel 𝐴 ∧ 𝐵 ∈ 𝐴) → ∩ ∩ 𝐵 ∈ dom 𝐴) | ||
Theorem | rneq 5799 | Equality theorem for range. (Contributed by NM, 29-Dec-1996.) |
⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵) | ||
Theorem | rneqi 5800 | Equality inference for range. (Contributed by NM, 4-Mar-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ran 𝐴 = ran 𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |