Home | Metamath
Proof Explorer Theorem List (p. 40 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 | inssdif0 3901 | Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅) | ||
Theorem | difid 3902 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | difidALT 3903 | Alternate proof of difid 3902. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | dif0 3904 | The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ ∅) = 𝐴 | ||
Theorem | ab0 3905 | The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 3908 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne 2782). (Contributed by BJ, 19-Mar-2021.) |
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | dfnf5 3906 | Characterization of non-freeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = ∅ ∨ {𝑥 ∣ 𝜑} = V)) | ||
Theorem | ab0orv 3907* | The class builder of a wff not containing the abstraction variable is either the empty set or the universal class. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.) |
⊢ ({𝑥 ∣ 𝜑} = ∅ ∨ {𝑥 ∣ 𝜑} = V) | ||
Theorem | abn0 3908 | Nonempty class abstraction. See also ab0 3905. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) | ||
Theorem | rab0 3909 | Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ | ||
Theorem | rab0OLD 3910 | Obsolete proof of rab0 3909 as of 14-Jul-2021. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ | ||
Theorem | rabeq0 3911 | Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | rabn0 3912 | Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabn0OLD 3913 | Obsolete proof of rabn0 3912 as of 16-Jul-2021. (Contributed by NM, 29-Aug-1999.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabeq0OLD 3914 | Obsolete proof of rabeq0 3911 as of 16-Jul-2021. (Contributed by Jeff Madsen, 7-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | rabxm 3915* | Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) | ||
Theorem | rabnc 3916* | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ | ||
Theorem | elneldisj 3917* | The set of elements containing a special element and the set of elements not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝑠} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝑠} ⇒ ⊢ (𝐸 ∩ 𝑁) = ∅ | ||
Theorem | elnelun 3918* | The union of the set of elements containing a special element and of the set of elements not containing the special element yields the original set. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝑠} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝑠} ⇒ ⊢ (𝐸 ∪ 𝑁) = 𝐴 | ||
Theorem | un0 3919 | The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 ∪ ∅) = 𝐴 | ||
Theorem | in0 3920 | The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∩ ∅) = ∅ | ||
Theorem | 0in 3921 | The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (∅ ∩ 𝐴) = ∅ | ||
Theorem | inv1 3922 | The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∩ V) = 𝐴 | ||
Theorem | unv 3923 | The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∪ V) = V | ||
Theorem | 0ss 3924 | The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.) |
⊢ ∅ ⊆ 𝐴 | ||
Theorem | ss0b 3925 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | ||
Theorem | ss0 3926 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | ||
Theorem | sseq0 3927 | A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | ||
Theorem | ssn0 3928 | A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | ||
Theorem | 0dif 3929 | The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
⊢ (∅ ∖ 𝐴) = ∅ | ||
Theorem | abf 3930 | A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | eq0rdv 3931* | Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | csbprc 3932 | The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) (Proof shortened by JJ, 27-Aug-2021.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | csbprcOLD 3933 | Obsolete proof of csbprc 3932 as of 27-Aug-2021. (Contributed by NM, 17-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | csb0 3934 | The proper substitution of a class into the empty set is empty. (Contributed by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅ | ||
Theorem | sbcel12 3935 | Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceqg 3936 | Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcnel12g 3937 | Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcne12 3938 | Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcel1g 3939* | Move proper substitution in and out of a membership relation. Note that the scope of [𝐴 / 𝑥] is the wff 𝐵 ∈ 𝐶, whereas the scope of ⦋𝐴 / 𝑥⦌ is the class 𝐵. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝐶)) | ||
Theorem | sbceq1g 3940* | Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | sbcel2 3941* | Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceq2g 3942* | Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | csbeq2d 3943 | Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2dv 3944* | Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbeq2i 3945 | Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 | ||
Theorem | csbcom 3946* | Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 | ||
Theorem | sbcnestgf 3947 | Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestgf 3948 | Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcnestg 3949* | Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestg 3950* | Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcco3g 3951* | Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑)) | ||
Theorem | csbco3g 3952* | Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷) | ||
Theorem | csbnest1g 3953 | Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbidm 3954* | Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbvarg 3955 | The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) | ||
Theorem | sbccsb 3956* | Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑}) | ||
Theorem | sbccsb2 3957 | Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑}) | ||
Theorem | rspcsbela 3958* | Special case related to rspsbc 3484. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) | ||
Theorem | sbnfc2 3959* | Two ways of expressing "𝑥 is (effectively) not free in 𝐴." (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) | ||
Theorem | csbab 3960* | Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbun 3961 | Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∪ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∪ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbin 3962 | Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | un00 3963 | Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) | ||
Theorem | vss 3964 | Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (V ⊆ 𝐴 ↔ 𝐴 = V) | ||
Theorem | 0pss 3965 | The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.) |
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅) | ||
Theorem | npss0 3966 | No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ¬ 𝐴 ⊊ ∅ | ||
Theorem | npss0OLD 3967 | Obsolete proof of npss0 3966 as of 14-Jul-2021. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ¬ 𝐴 ⊊ ∅ | ||
Theorem | pssv 3968 | Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V) | ||
Theorem | disj 3969* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | disjr 3970* | Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | disj1 3971* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | reldisj 3972 | Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) | ||
Theorem | disj3 3973 | Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) | ||
Theorem | disjne 3974 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷) | ||
Theorem | disjel 3975 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | disj2 3976 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵)) | ||
Theorem | disj4 3977 | Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴) | ||
Theorem | ssdisj 3978 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | ssdisjOLD 3979 | Obsolete proof of ssdisj 3978 as of 14-Jul-2021. (Contributed by FL, 24-Jan-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | disjpss 3980 | A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | undisj1 3981 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) | ||
Theorem | undisj2 3982 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅) | ||
Theorem | ssindif0 3983 | Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅) | ||
Theorem | inelcm 3984 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | ||
Theorem | minel 3985 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | minelOLD 3986 | Obsolete proof of minel 3985 as of 14-Jul-2021. (Contributed by NM, 22-Jun-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | undif4 3987 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) | ||
Theorem | disjssun 3988 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) | ||
Theorem | vdif0 3989 | Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅) | ||
Theorem | difrab0eq 3990* | If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ ((𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅ ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑}) | ||
Theorem | pssnel 3991* | A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | ||
Theorem | disjdif 3992 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | difin0 3993 | The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ | ||
Theorem | unvdif 3994 | The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (V ∖ 𝐴)) = V | ||
Theorem | undif1 3995 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3992). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) | ||
Theorem | undif2 3996 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3992). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | ||
Theorem | undifabs 3997 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundif 3998 | The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | disjdif2 3999 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 4000 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |