Home | Metamath
Proof Explorer Theorem List (p. 42 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-28687) |
Hilbert Space Explorer
(28688-30210) |
Users' Mathboxes
(30211-44897) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eldifi 4101 | Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | eldifn 4102 | Implication of membership in a class difference. (Contributed by NM, 3-May-1994.) |
⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | elndif 4103 | A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵)) | ||
Theorem | neldif 4104 | Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ (𝐵 ∖ 𝐶)) → 𝐴 ∈ 𝐶) | ||
Theorem | difdif 4105 | Double class difference. Exercise 11 of [TakeutiZaring] p. 22. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐴)) = 𝐴 | ||
Theorem | difss 4106 | Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 | ||
Theorem | difssd 4107 | A difference of two classes is contained in the minuend. Deduction form of difss 4106. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) | ||
Theorem | difss2 4108 | If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | ||
Theorem | difss2d 4109 | If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4108. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ssdifss 4110 | Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ddif 4111 | Double complement under universal class. Exercise 4.10(s) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (V ∖ (V ∖ 𝐴)) = 𝐴 | ||
Theorem | ssconb 4112 | Contraposition law for subsets. (Contributed by NM, 22-Mar-1998.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴))) | ||
Theorem | sscon 4113 | Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdif 4114 | Difference law for subsets. (Contributed by NM, 28-May-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | ssdifd 4115 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4114. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | sscond 4116 | If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4113. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | ||
Theorem | ssdifssd 4117 | If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4110. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | ssdif2d 4118 | If 𝐴 is contained in 𝐵 and 𝐶 is contained in 𝐷, then (𝐴 ∖ 𝐷) is contained in (𝐵 ∖ 𝐶). Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ (𝐵 ∖ 𝐶)) | ||
Theorem | raldifb 4119 | Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∉ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
Theorem | rexdifi 4120 | Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 ¬ 𝜑) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)𝜑) | ||
Theorem | complss 4121 | Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 19-Mar-2021.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ (V ∖ 𝐴)) | ||
Theorem | compleq 4122 | Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021.) |
⊢ (𝐴 = 𝐵 ↔ (V ∖ 𝐴) = (V ∖ 𝐵)) | ||
Theorem | elun 4123 | Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∈ (𝐵 ∪ 𝐶) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ 𝐶)) | ||
Theorem | elunnel1 4124 | A member of a union that is not member of the first class, is member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ (𝐵 ∪ 𝐶) ∧ ¬ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | uneqri 4125* | Inference from membership to union. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∪ 𝐵) = 𝐶 | ||
Theorem | unidm 4126 | Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∪ 𝐴) = 𝐴 | ||
Theorem | uncom 4127 | Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | ||
Theorem | equncom 4128 | If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4128 was automatically derived from equncomVD 41193 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | ||
Theorem | equncomi 4129 | Inference form of equncom 4128. equncomi 4129 was automatically derived from equncomiVD 41194 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
⊢ 𝐴 = (𝐵 ∪ 𝐶) ⇒ ⊢ 𝐴 = (𝐶 ∪ 𝐵) | ||
Theorem | uneq1 4130 | Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2 4131 | Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12 4132 | Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | uneq1i 4133 | Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) | ||
Theorem | uneq2i 4134 | Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵) | ||
Theorem | uneq12i 4135 | Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷) | ||
Theorem | uneq1d 4136 | Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)) | ||
Theorem | uneq2d 4137 | Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)) | ||
Theorem | uneq12d 4138 | Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)) | ||
Theorem | nfun 4139 | Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵) | ||
Theorem | unass 4140 | Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | un12 4141 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | un23 4142 | A rearrangement of union. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ 𝐵) | ||
Theorem | un4 4143 | A rearrangement of the union of 4 classes. (Contributed by NM, 12-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ (𝐶 ∪ 𝐷)) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐷)) | ||
Theorem | unundi 4144 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∪ (𝐴 ∪ 𝐶)) | ||
Theorem | unundir 4145 | Union distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∪ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun1 4146 | Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | ssun2 4147 | Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴) | ||
Theorem | ssun3 4148 | Subclass law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssun4 4149 | Subclass law for union of classes. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | elun1 4150 | Membership law for union of classes. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶)) | ||
Theorem | elun2 4151 | Membership law for union of classes. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵)) | ||
Theorem | elunant 4152 | 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 4153 | Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | ssequn1 4154 | 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 4155 | Subclass law for union of classes. Exercise 7 of [TakeutiZaring] p. 18. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∪ 𝐴) ⊆ (𝐶 ∪ 𝐵)) | ||
Theorem | unss12 4156 | Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | ||
Theorem | ssequn2 4157 | A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵) | ||
Theorem | unss 4158 | 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 4159 | An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶 | ||
Theorem | unssd 4160 | A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | ||
Theorem | unssad 4161 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4158. Partial converse of unssd 4160. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | ||
Theorem | unssbd 4162 | If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4158. Partial converse of unssd 4160. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | ||
Theorem | ssun 4163 | A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ (𝐵 ∪ 𝐶)) | ||
Theorem | rexun 4164 | Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralunb 4165 | Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ralun 4166 | Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑) | ||
Theorem | elin 4167 | Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | elini 4168 | Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ 𝐴 ∈ 𝐶 ⇒ ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | elind 4169 | Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) | ||
Theorem | elinel1 4170 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵) | ||
Theorem | elinel2 4171 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | elin2 4172 | Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = (𝐵 ∩ 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | elin1d 4173 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐴) | ||
Theorem | elin2d 4174 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
Theorem | elin3 4175 | Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) | ||
Theorem | incom 4176 | 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 4177 | Obsolete version of incom 4176 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 4178* | Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∩ 𝐵) = 𝐶 | ||
Theorem | ineq1 4179 | Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq1OLD 4180 | Obsolete version of ineq1 4179 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 4181 | Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12 4182 | Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineq1i 4183 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) | ||
Theorem | ineq2i 4184 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) | ||
Theorem | ineq12i 4185 | Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) | ||
Theorem | ineq1d 4186 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
Theorem | ineq2d 4187 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
Theorem | ineq12d 4188 | Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | ineqan12d 4189 | Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
Theorem | sseqin2 4190 | A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
Theorem | nfin 4191 | Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) | ||
Theorem | rabbi2dva 4192* | Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | inidm 4193 | Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ∩ 𝐴) = 𝐴 | ||
Theorem | inass 4194 | Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | in12 4195 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | in32 4196 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵) | ||
Theorem | in13 4197 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴)) | ||
Theorem | in31 4198 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴) | ||
Theorem | inrot 4199 | Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵) | ||
Theorem | in4 4200 | Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.) |
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |