Home | Metamath
Proof Explorer Theorem List (p. 42 of 465) | < 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-29266) |
Hilbert Space Explorer
(29267-30789) |
Users' Mathboxes
(30790-46477) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | un12 4101 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | un23 4102 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) | ||
Theorem | un4 4103 | A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) | ||
Theorem | unundi 4104 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | unundir 4105 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun1 4106 | Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ssun2 4107 | Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) | ||
Theorem | ssun3 4108 | Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun4 4109 | Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | elun1 4110 | Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) | ||
Theorem | elun2 4111 | Membership law for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵)) | ||
Theorem | elunant 4112 | A statement is true for every element of the union of a pair of classes if and only if it is true for every element of the first class and for every element of the second class. (Contributed by BTernaryTau, 27-Sep-2023.) |
⊢ ((𝐶 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝐶 ∈ 𝐴 → 𝜑) ∧ (𝐶 ∈ 𝐵 → 𝜑))) | ||
Theorem | unss1 4113 | Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssequn1 4114 | A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) | ||
Theorem | unss2 4115 | Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | unss12 4116 | Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | ||
Theorem | ssequn2 4117 | A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) | ||
Theorem | unss 4118 | The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
Theorem | unssi 4119 | An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 | ||
Theorem | unssd 4120 | A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
Theorem | unssad 4121 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4118. Partial converse of unssd 4120. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | unssbd 4122 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4118. Partial converse of unssd 4120. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | ssun 4123 | A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | rexun 4124 | Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralunb 4125 | Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralun 4126 | Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) | ||
Theorem | elini 4127 | Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | elind 4128 | Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) | ||
Theorem | elinel1 4129 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | elinel2 4130 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | elin2 4131 | Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = (𝐵 ∩ 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | elin1d 4132 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐴) | ||
Theorem | elin2d 4133 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
Theorem | elin3 4134 | Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) | ||
Theorem | incom 4135 | Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by SN, 12-Dec-2023.) |
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) | ||
Theorem | incomOLD 4136 | Obsolete version of incom 4135 as of 12-Dec-2023. Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) | ||
Theorem | ineqcom 4137 | Two ways of expressing that two classes have a given intersection. This is often used when that given intersection is the empty set, in which case the statement displays two ways of expressing that two classes are disjoint (when 𝐶 = ∅: ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)). (Contributed by Peter Mazsa, 22-Mar-2017.) |
⊢ ((𝐴 ∩ 𝐵) = 𝐶 ↔ (𝐵 ∩ 𝐴) = 𝐶) | ||
Theorem | ineqcomi 4138 | Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4137. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.) |
⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝐵 ∩ 𝐴) = 𝐶 | ||
Theorem | ineqri 4139* | Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∩ 𝐵) = 𝐶 | ||
Theorem | ineq1 4140 | Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq2 4141 | Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12 4142 | Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineq1i 4143 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) | ||
Theorem | ineq2i 4144 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) | ||
Theorem | ineq12i 4145 | Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) | ||
Theorem | ineq1d 4146 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq2d 4147 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12d 4148 | Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineqan12d 4149 | Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | sseqin2 4150 | A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
Theorem | nfin 4151 | Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) | ||
Theorem | rabbi2dva 4152* | Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | inidm 4153 | Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∩ 𝐴) = 𝐴 | ||
Theorem | inass 4154 | Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | in12 4155 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | in32 4156 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵) | ||
Theorem | in13 4157 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴)) | ||
Theorem | in31 4158 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴) | ||
Theorem | inrot 4159 | Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵) | ||
Theorem | in4 4160 | Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.) |
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) | ||
Theorem | inindi 4161 | Intersection distributes over itself. (Contributed by NM, 6-May-1994.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | inindir 4162 | Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | inss1 4163 | The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | ||
Theorem | inss2 4164 | The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | ||
Theorem | ssin 4165 | Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ssini 4166 | An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) | ||
Theorem | ssind 4167 | A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ssrin 4168 | Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | sslin 4169 | Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) | ||
Theorem | ssrind 4170 | Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ss2in 4171 | Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | ||
Theorem | ssinss1 4172 | Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | inss 4173 | Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | rexin 4174 | Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.) |
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | dfss7 4175* | Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.) |
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵) | ||
Syntax | csymdif 4176 | Declare the syntax for symmetric difference. |
class (𝐴 △ 𝐵) | ||
Definition | df-symdif 4177 | Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4185, dfsymdif3 4231 and dfsymdif4 4183. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) | ||
Theorem | symdifcom 4178 | Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴) | ||
Theorem | symdifeq1 4179 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶)) | ||
Theorem | symdifeq2 4180 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵)) | ||
Theorem | nfsymdif 4181 | Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 △ 𝐵) | ||
Theorem | elsymdif 4182 | Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) | ||
Theorem | dfsymdif4 4183* | Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.) |
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)} | ||
Theorem | elsymdifxor 4184 | Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020.) (Proof shortened by BJ, 13-Aug-2022.) |
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ (𝐴 ∈ 𝐵 ⊻ 𝐴 ∈ 𝐶)) | ||
Theorem | dfsymdif2 4185* | Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.) |
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} | ||
Theorem | symdifass 4186 | Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.) |
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶)) | ||
Theorem | difsssymdif 4187 | The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.) |
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵) | ||
Theorem | difsymssdifssd 4188 | If the symmetric difference is contained in 𝐶, so is one of the differences. (Contributed by AV, 17-Aug-2022.) |
⊢ (𝜑 → (𝐴 △ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | unabs 4189 | Absorption law for union. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 | ||
Theorem | inabs 4190 | Absorption law for intersection. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 | ||
Theorem | nssinpss 4191 | Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) ⊊ 𝐴) | ||
Theorem | nsspssun 4192 | Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | dfss4 4193 | Subclass defined in terms of class difference. See comments under dfun2 4194. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) | ||
Theorem | dfun2 4194 | An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4195 and dfss4 4193 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation ∖ (class difference). (Contributed by NM, 10-Jun-2004.) |
⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) | ||
Theorem | dfin2 4195 | An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4194. Another version is given by dfin4 4202. (Contributed by NM, 10-Jun-2004.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) | ||
Theorem | difin 4196 | Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | ssdifim 4197 | Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵)) | ||
Theorem | ssdifsym 4198 | Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵))) | ||
Theorem | dfss5 4199* | Alternate definition of subclass relationship: a class 𝐴 is a subclass of another class 𝐵 iff each element of 𝐴 is equal to an element of 𝐵. (Contributed by AV, 13-Nov-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝑦) | ||
Theorem | dfun3 4200 | Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |