| Metamath
Proof Explorer Theorem List (p. 43 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elinel1 4201 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵) | ||
| Theorem | elinel2 4202 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶) | ||
| Theorem | elin2 4203 | Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝑋 = (𝐵 ∩ 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
| Theorem | elin1d 4204 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐴) | ||
| Theorem | elin2d 4205 | Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | elin3 4206 | Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
| ⊢ 𝑋 = ((𝐵 ∩ 𝐶) ∩ 𝐷) ⇒ ⊢ (𝐴 ∈ 𝑋 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐷)) | ||
| Theorem | nel1nelin 4207 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
| Theorem | nel2nelin 4208 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
| Theorem | incom 4209 | 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 | ineqcom 4210 | 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 4211 | Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4210. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.) |
| ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝐵 ∩ 𝐴) = 𝐶 | ||
| Theorem | ineqri 4212* | Inference from membership to intersection. (Contributed by NM, 21-Jun-1993.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ⇒ ⊢ (𝐴 ∩ 𝐵) = 𝐶 | ||
| Theorem | ineq1 4213 | Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.) (Proof shortened by SN, 20-Sep-2023.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
| Theorem | ineq2 4214 | Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
| Theorem | ineq12 4215 | Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
| Theorem | ineq1i 4216 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) | ||
| Theorem | ineq2i 4217 | Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵) | ||
| Theorem | ineq12i 4218 | Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) | ||
| Theorem | ineq1d 4219 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | ||
| Theorem | ineq2d 4220 | Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)) | ||
| Theorem | ineq12d 4221 | Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
| Theorem | ineqan12d 4222 | Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | ||
| Theorem | sseqin2 4223 | A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | ||
| Theorem | nfin 4224 | Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 14-May-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) | ||
| Theorem | nfinOLD 4225 | Obsolete version of nfin 4224 as of 14-May-2025. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) | ||
| Theorem | rabbi2dva 4226* | Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
| Theorem | inidm 4227 | Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.) |
| ⊢ (𝐴 ∩ 𝐴) = 𝐴 | ||
| Theorem | inass 4228 | Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) | ||
| Theorem | in12 4229 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) |
| ⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐴 ∩ 𝐶)) | ||
| Theorem | in32 4230 | A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ 𝐵) | ||
| Theorem | in13 4231 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
| ⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐶 ∩ (𝐵 ∩ 𝐴)) | ||
| Theorem | in31 4232 | A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐵) ∩ 𝐴) | ||
| Theorem | inrot 4233 | Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐶 ∩ 𝐴) ∩ 𝐵) | ||
| Theorem | in4 4234 | Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) | ||
| Theorem | inindi 4235 | Intersection distributes over itself. (Contributed by NM, 6-May-1994.) |
| ⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶)) | ||
| Theorem | inindir 4236 | Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.) |
| ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | ||
| Theorem | inss1 4237 | 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 4238 | 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 4239 | 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 4240 | An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.) |
| ⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) | ||
| Theorem | ssind 4241 | 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 4242 | Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
| Theorem | sslin 4243 | Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) | ||
| Theorem | ssrind 4244 | Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
| Theorem | ss2in 4245 | Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | ||
| Theorem | ssinss1 4246 | Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) |
| ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
| Theorem | ssinss1d 4247 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
| Theorem | inss 4248 | Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
| Theorem | ralin 4249 | Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023.) |
| ⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑)) | ||
| Theorem | rexin 4250 | Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.) |
| ⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
| Theorem | dfss7 4251* | Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.) |
| ⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵) | ||
| Syntax | csymdif 4252 | Declare the syntax for symmetric difference. |
| class (𝐴 △ 𝐵) | ||
| Definition | df-symdif 4253 | Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4261, dfsymdif3 4306 and dfsymdif4 4259. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) | ||
| Theorem | symdifcom 4254 | Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.) |
| ⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴) | ||
| Theorem | symdifeq1 4255 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶)) | ||
| Theorem | symdifeq2 4256 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵)) | ||
| Theorem | nfsymdif 4257 | Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 △ 𝐵) | ||
| Theorem | elsymdif 4258 | Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) | ||
| Theorem | dfsymdif4 4259* | Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.) |
| ⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)} | ||
| Theorem | elsymdifxor 4260 | 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 4261* | Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.) |
| ⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} | ||
| Theorem | symdifass 4262 | Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.) |
| ⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶)) | ||
| Theorem | difsssymdif 4263 | The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.) |
| ⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵) | ||
| Theorem | difsymssdifssd 4264 | If the symmetric difference is contained in 𝐶, so is one of the differences. (Contributed by AV, 17-Aug-2022.) |
| ⊢ (𝜑 → (𝐴 △ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
| Theorem | unabs 4265 | Absorption law for union. (Contributed by NM, 16-Apr-2006.) |
| ⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 | ||
| Theorem | inabs 4266 | Absorption law for intersection. (Contributed by NM, 16-Apr-2006.) |
| ⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 | ||
| Theorem | nssinpss 4267 | 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 4268 | Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.) |
| ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵)) | ||
| Theorem | dfss4 4269 | Subclass defined in terms of class difference. See comments under dfun2 4270. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) | ||
| Theorem | dfun2 4270 | An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4271 and dfss4 4269 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 4271 | An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4270. Another version is given by dfin4 4278. (Contributed by NM, 10-Jun-2004.) |
| ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) | ||
| Theorem | difin 4272 | 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 4273 | Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.) |
| ⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵)) | ||
| Theorem | ssdifsym 4274 | Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.) |
| ⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵))) | ||
| Theorem | dfss5 4275* | 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 4276 | 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 4277 | 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 4278 | Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.) |
| ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) | ||
| Theorem | invdif 4279 | Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.) |
| ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
| Theorem | indif 4280 | Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
| ⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
| Theorem | indif2 4281 | Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.) |
| ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
| Theorem | indif1 4282 | Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
| Theorem | indifcom 4283 | Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) | ||
| Theorem | indi 4284 | 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.) |
| ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
| Theorem | undi 4285 | Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶)) | ||
| Theorem | indir 4286 | Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
| ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) | ||
| Theorem | undir 4287 | Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
| ⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) | ||
| Theorem | unineq 4288 | Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.) |
| ⊢ (((𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) ↔ 𝐴 = 𝐵) | ||
| Theorem | uneqin 4289 | Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) | ||
| Theorem | difundi 4290 | Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
| ⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) | ||
| Theorem | difundir 4291 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
| ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | ||
| Theorem | difindi 4292 | Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
| ⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | ||
| Theorem | difindir 4293 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
| ⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) | ||
| Theorem | indifdi 4294 | Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024.) |
| ⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ (𝐴 ∩ 𝐶)) | ||
| Theorem | indifdir 4295 | Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by BTernaryTau, 14-Aug-2024.) |
| ⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) | ||
| Theorem | difdif2 4296 | Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
| ⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
| Theorem | undm 4297 | De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.) |
| ⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵)) | ||
| Theorem | indm 4298 | De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.) |
| ⊢ (V ∖ (𝐴 ∩ 𝐵)) = ((V ∖ 𝐴) ∪ (V ∖ 𝐵)) | ||
| Theorem | difun1 4299 | A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.) |
| ⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) | ||
| Theorem | undif3 4300 | An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.) |
| ⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |