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