Home | Metamath
Proof Explorer Theorem List (p. 43 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | in4 4201 | Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.) |
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐷)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐷)) | ||
Theorem | inindi 4202 | Intersection distributes over itself. (Contributed by NM, 6-May-1994.) |
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ (𝐴 ∩ 𝐶)) | ||
Theorem | inindir 4203 | Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | ||
Theorem | inss1 4204 | 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 4205 | 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 4206 | 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 4207 | An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.) |
⊢ 𝐴 ⊆ 𝐵 & ⊢ 𝐴 ⊆ 𝐶 ⇒ ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶) | ||
Theorem | ssind 4208 | 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 4209 | Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | sslin 4210 | Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) | ||
Theorem | ssrind 4211 | Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | ||
Theorem | ss2in 4212 | Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | ||
Theorem | ssinss1 4213 | Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | inss 4214 | Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | rexin 4215 | Restricted existential quantification over intersection. (Contributed by Peter Mazsa, 17-Dec-2018.) |
⊢ (∃𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | dfss7 4216* | Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022.) |
⊢ (𝐵 ⊆ 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = 𝐵) | ||
Syntax | csymdif 4217 | Declare the syntax for symmetric difference. |
class (𝐴 △ 𝐵) | ||
Definition | df-symdif 4218 | Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 4226, dfsymdif3 4268 and dfsymdif4 4224. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) | ||
Theorem | symdifcom 4219 | Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴) | ||
Theorem | symdifeq1 4220 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶)) | ||
Theorem | symdifeq2 4221 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵)) | ||
Theorem | nfsymdif 4222 | Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 △ 𝐵) | ||
Theorem | elsymdif 4223 | Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) | ||
Theorem | dfsymdif4 4224* | Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004.) (Revised by AV, 17-Aug-2022.) |
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)} | ||
Theorem | elsymdifxor 4225 | 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 4226* | Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.) |
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} | ||
Theorem | symdifass 4227 | Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by BJ, 7-Sep-2022.) |
⊢ ((𝐴 △ 𝐵) △ 𝐶) = (𝐴 △ (𝐵 △ 𝐶)) | ||
Theorem | difsssymdif 4228 | The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022.) |
⊢ (𝐴 ∖ 𝐵) ⊆ (𝐴 △ 𝐵) | ||
Theorem | difsymssdifssd 4229 | If the symmetric difference is contained in 𝐶, so is one of the differences. (Contributed by AV, 17-Aug-2022.) |
⊢ (𝜑 → (𝐴 △ 𝐵) ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | unabs 4230 | Absorption law for union. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 | ||
Theorem | inabs 4231 | Absorption law for intersection. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 | ||
Theorem | nssinpss 4232 | 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 4233 | Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | dfss4 4234 | Subclass defined in terms of class difference. See comments under dfun2 4235. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) | ||
Theorem | dfun2 4235 | An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 4236 and dfss4 4234 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 4236 | An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4235. Another version is given by dfin4 4243. (Contributed by NM, 10-Jun-2004.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) | ||
Theorem | difin 4237 | 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 4238 | Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵)) | ||
Theorem | ssdifsym 4239 | Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵))) | ||
Theorem | dfss5 4240* | 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 4241 | 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 4242 | 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 4243 | Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) | ||
Theorem | invdif 4244 | Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif 4245 | Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif2 4246 | Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indif1 4247 | Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indifcom 4248 | Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | indi 4249 | 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 4250 | 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 4251 | Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) | ||
Theorem | undir 4252 | Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) | ||
Theorem | unineq 4253 | 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 4254 | 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 4255 | Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | difundir 4256 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | ||
Theorem | difindi 4257 | Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | ||
Theorem | difindir 4258 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) | ||
Theorem | indifdir 4259 | Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) |
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | difdif2 4260 | Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
Theorem | undm 4261 | 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 4262 | 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 4263 | A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) | ||
Theorem | undif3 4264 | 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.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) | ||
Theorem | difin2 4265 | Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) | ||
Theorem | dif32 4266 | Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) | ||
Theorem | difabs 4267 | Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | dfsymdif3 4268 | Alternate definition of the symmetric difference, given in Example 4.1 of [Stoll] p. 262 (the original definition corresponds to [Stoll] p. 13). (Contributed by NM, 17-Aug-2004.) (Revised by BJ, 30-Apr-2020.) |
⊢ (𝐴 △ 𝐵) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵)) | ||
Theorem | unab 4269 | Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inab 4270 | Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difab 4271 | Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | notab 4272 | A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.) |
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) | ||
Theorem | unrab 4273 | Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inrab 4274 | Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | inrab2 4275* | Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} | ||
Theorem | difrab 4276 | Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | dfrab3 4277* | Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfrab2 4278* | Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) | ||
Theorem | notrab 4279* | Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} | ||
Theorem | dfrab3ss 4280* | Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.) |
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑})) | ||
Theorem | rabun2 4281 | Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | reuss2 4282* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuss 4283* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuun1 4284* | Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuun2 4285* | Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) |
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reupick 4286* | Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | reupick3 4287* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | ||
Theorem | reupick2 4288* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) | ||
Theorem | euelss 4289* | Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
Syntax | c0 4290 | Extend class notation to include the empty set. |
class ∅ | ||
Definition | df-nul 4291 | Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5202 that an empty set exists. Then, by uniqueness among classes (eq0 4307, as opposed to the weaker uniqueness among sets, nulmo 2798), it will follow that ∅ is indeed a set (0ex 5203). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4292. (Contributed by NM, 17-Jun-1993.) Clarify that at this point, it is not established that it is a set. (Revised by BJ, 22-Sep-2022.) |
⊢ ∅ = (V ∖ V) | ||
Theorem | dfnul2 4292 | Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2136, ax-11 2151, and ax-12 2167. (Revised by Steven Nguyen, 3-May-2023.) |
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
Theorem | dfnul2OLD 4293 | Obsolete version of dfnul2 4292 as of 3-May-2023. Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
Theorem | dfnul3 4294 | Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) |
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | ||
Theorem | noel 4295 | The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) Remove dependency on ax-10 2136, ax-11 2151, and ax-12 2167. (Revised by Steven Nguyen, 3-May-2023.) |
⊢ ¬ 𝐴 ∈ ∅ | ||
Theorem | noelOLD 4296 | Obsolete version of noel 4295 as of 3-May-2023. The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ¬ 𝐴 ∈ ∅ | ||
Theorem | nel02 4297 | The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.) |
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | n0i 4298 | If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | ||
Theorem | ne0i 4299 | If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | ne0d 4300 | Deduction form of ne0i 4299. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |