Home | Metamath
Proof Explorer Theorem List (p. 39 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sslin 3801 | Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) | ||
Theorem | ss2in 3802 | Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | ||
Theorem | ssinss1 3803 | Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Theorem | inss 3804 | Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∨ 𝐵 ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | ||
Syntax | csymdif 3805 | Declare the syntax for symmetric difference. |
class (𝐴 △ 𝐵) | ||
Definition | df-symdif 3806 | Define the symmetric difference of two classes. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 △ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) | ||
Theorem | symdifcom 3807 | Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ 𝐵) = (𝐵 △ 𝐴) | ||
Theorem | symdifeq1 3808 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐴 △ 𝐶) = (𝐵 △ 𝐶)) | ||
Theorem | symdifeq2 3809 | Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 = 𝐵 → (𝐶 △ 𝐴) = (𝐶 △ 𝐵)) | ||
Theorem | nfsymdif 3810 | Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 △ 𝐵) | ||
Theorem | elsymdif 3811 | Membership in a symmetric difference. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) | ||
Theorem | elsymdifxor 3812 | Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020.) |
⊢ (𝐴 ∈ (𝐵 △ 𝐶) ↔ (𝐴 ∈ 𝐵 ⊻ 𝐴 ∈ 𝐶)) | ||
Theorem | dfsymdif2 3813* | Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020.) |
⊢ (𝐴 △ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)} | ||
Theorem | symdif2 3814* | Two ways to express symmetric difference. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)} | ||
Theorem | symdifass 3815 | Symmetric difference associates. (Contributed by Scott Fenton, 24-Apr-2012.) |
⊢ (𝐴 △ (𝐵 △ 𝐶)) = ((𝐴 △ 𝐵) △ 𝐶) | ||
Theorem | unabs 3816 | Absorption law for union. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 | ||
Theorem | inabs 3817 | Absorption law for intersection. (Contributed by NM, 16-Apr-2006.) |
⊢ (𝐴 ∩ (𝐴 ∪ 𝐵)) = 𝐴 | ||
Theorem | nssinpss 3818 | 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 3819 | Negation of subclass expressed in terms of proper subclass and union. (Contributed by NM, 15-Sep-2004.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ 𝐵 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | dfss4 3820 | Subclass defined in terms of class difference. See comments under dfun2 3821. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) | ||
Theorem | dfun2 3821 | An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3822 and dfss4 3820 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 3822 | An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 3821. Another version is given by dfin4 3826. (Contributed by NM, 10-Jun-2004.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) | ||
Theorem | difin 3823 | Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | dfun3 3824 | 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 3825 | 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 3826 | Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) | ||
Theorem | invdif 3827 | Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif 3828 | Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif2 3829 | Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indif1 3830 | Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indifcom 3831 | Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | indi 3832 | 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 3833 | 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 3834 | Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) | ||
Theorem | undir 3835 | Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) | ||
Theorem | unineq 3836 | 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 3837 | 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 3838 | Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | difundir 3839 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | ||
Theorem | difindi 3840 | Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | ||
Theorem | difindir 3841 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) | ||
Theorem | indifdir 3842 | Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) |
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | difdif2 3843 | Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
Theorem | undm 3844 | 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 3845 | 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 3846 | A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) | ||
Theorem | undif3 3847 | 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 | undif3OLD 3848 | Obsolete proof of undif3 3847 as of 13-Jul-2021. (Contributed by Alan Sare, 17-Apr-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) | ||
Theorem | difin2 3849 | Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) | ||
Theorem | dif32 3850 | Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) | ||
Theorem | difabs 3851 | Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | dfsymdif3 3852 | 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 3853 | Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inab 3854 | Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difab 3855 | Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | notab 3856 | A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.) |
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) | ||
Theorem | unrab 3857 | Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inrab 3858 | Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | inrab2 3859* | Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} | ||
Theorem | difrab 3860 | Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | dfrab3 3861* | Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfrab2 3862* | Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) | ||
Theorem | notrab 3863* | Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} | ||
Theorem | dfrab3ss 3864* | 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 3865 | Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | reuss2 3866* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuss 3867* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuun1 3868* | Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuun2 3869* | Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) |
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reupick 3870* | Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | reupick3 3871* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | ||
Theorem | reupick2 3872* | 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 3873* | Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
Syntax | c0 3874 | Extend class notation to include the empty set. |
class ∅ | ||
Definition | df-nul 3875 | Define the empty set. Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 3876. (Contributed by NM, 17-Jun-1993.) |
⊢ ∅ = (V ∖ V) | ||
Theorem | dfnul2 3876 | Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) |
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
Theorem | dfnul3 3877 | Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) |
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | ||
Theorem | noel 3878 | 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.) |
⊢ ¬ 𝐴 ∈ ∅ | ||
Theorem | n0i 3879 | If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | ||
Theorem | ne0i 3880 | If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | n0ii 3881 | If a set has elements, then it is not empty. Inference associated with n0i 3879. (Contributed by BJ, 15-Jul-2021.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ | ||
Theorem | ne0ii 3882 | If a set has elements, then it is not empty. Inference associated with ne0i 3880. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ | ||
Theorem | vn0 3883 | The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) |
⊢ V ≠ ∅ | ||
Theorem | eq0f 3884 | The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0f 3885 | A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of neq0 3889 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0f 3886 | A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 3890 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0fOLD 3887 | Obsolete proof of n0f 3886 as of 15-Jul-2021. (Contributed by NM, 17-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eq0 3888* | The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0 3889* | A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) |
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0 3890* | A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | reximdva0 3891* | Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rspn0 3892* | Specialization for restricted generalization with a nonempty set. (Contributed by Alexander van der Vekens, 6-Sep-2018.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
Theorem | n0moeu 3893* | A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.) |
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | rex0 3894 | Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.) |
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 | ||
Theorem | 0el 3895* | Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | ssdif0 3896 | Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) | ||
Theorem | difn0 3897 | If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵) | ||
Theorem | pssdifn0 3898 | A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | pssdif 3899 | A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | difin0ss 3900 | Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |