| Metamath
Proof Explorer Theorem List (p. 44 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 | difin2 4301 | Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) | ||
| Theorem | dif32 4302 | Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.) |
| ⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) | ||
| Theorem | difabs 4303 | Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.) |
| ⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
| Theorem | sscon34b 4304 | Relative complementation reverses inclusion of subclasses. Relativized version of complss 4151. (Contributed by RP, 3-Jun-2021.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))) | ||
| Theorem | rcompleq 4305 | Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4152. (Contributed by RP, 10-Jun-2021.) |
| ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))) | ||
| Theorem | dfsymdif3 4306 | 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 | unabw 4307* | Union of two class abstractions. Version of unab 4308 using implicit substitution, which does not require ax-8 2110, ax-10 2141, ax-12 2177. (Contributed by GG, 15-Oct-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) ⇒ ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑦 ∣ (𝜒 ∨ 𝜃)} | ||
| Theorem | unab 4308 | Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} | ||
| Theorem | inab 4309 | Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | difab 4310 | Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| ⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
| Theorem | abanssl 4311 | A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
| ⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜑} | ||
| Theorem | abanssr 4312 | A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
| ⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜓} | ||
| Theorem | notabw 4313* | A class abstraction defined by a negation. Version of notab 4314 using implicit substitution, which does not require ax-10 2141, ax-12 2177. (Contributed by GG, 15-Oct-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑦 ∣ 𝜓}) | ||
| Theorem | notab 4314 | A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.) |
| ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) | ||
| Theorem | unrab 4315 | Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} | ||
| Theorem | inrab 4316 | Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
| Theorem | inrab2 4317* | Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} | ||
| Theorem | difrab 4318 | Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
| Theorem | dfrab3 4319* | Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) | ||
| Theorem | dfrab2 4320* | Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.) |
| ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) | ||
| Theorem | rabdif 4321* | Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
| Theorem | notrab 4322* | Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.) |
| ⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} | ||
| Theorem | dfrab3ss 4323* | 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 4324 | Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
| ⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
| Theorem | reuun2 4325 | Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Wolf Lammen, 15-May-2025.) |
| ⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) | ||
| Theorem | reuss2 4326* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.) |
| ⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | reuss 4327* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | reuun1 4328* | Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.) |
| ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | reupick 4329* | Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.) |
| ⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
| Theorem | reupick3 4330* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.) |
| ⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | ||
| Theorem | reupick2 4331* | 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 4332* | Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
| Syntax | c0 4333 | Extend class notation to include the empty set. |
| class ∅ | ||
| Definition | df-nul 4334 | Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5306 that an empty set exists. Then, by uniqueness among classes (eq0 4350, as opposed to the weaker uniqueness among sets, nulmo 2713), it will follow that ∅ is indeed a set (0ex 5307). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4336. (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 | dfnul4 4335 | Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 4336. (Revised by BJ, 23-Sep-2024.) |
| ⊢ ∅ = {𝑥 ∣ ⊥} | ||
| Theorem | dfnul2 4336 | Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2141, ax-11 2157, and ax-12 2177. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
| ⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
| Theorem | dfnul3 4337 | Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.) |
| ⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | ||
| Theorem | noel 4338 | 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 2141, ax-11 2157, and ax-12 2177. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
| ⊢ ¬ 𝐴 ∈ ∅ | ||
| Theorem | nel02 4339 | The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.) |
| ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴) | ||
| Theorem | n0i 4340 | If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
| ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | ||
| Theorem | ne0i 4341 | If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.) |
| ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | ne0d 4342 | Deduction form of ne0i 4341. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
| Theorem | n0ii 4343 | If a class has elements, then it is not empty. Inference associated with n0i 4340. (Contributed by BJ, 15-Jul-2021.) |
| ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ | ||
| Theorem | ne0ii 4344 | If a class has elements, then it is nonempty. Inference associated with ne0i 4341. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ | ||
| Theorem | vn0 4345 | The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 6-Sep-2024.) |
| ⊢ V ≠ ∅ | ||
| Theorem | vn0ALT 4346 | Alternate proof of vn0 4345. Shorter, but requiring df-clel 2816, ax-8 2110. (Contributed by NM, 11-Sep-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ V ≠ ∅ | ||
| Theorem | eq0f 4347 | A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by BJ, 15-Jul-2021.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
| Theorem | neq0f 4348 | A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of neq0 4352 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | n0f 4349 | A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 4353 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | eq0 4350* | A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 6-Sep-2024.) |
| ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
| Theorem | eq0ALT 4351* | Alternate proof of eq0 4350. Shorter, but requiring df-clel 2816, ax-8 2110. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG and Steven Nguyen, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
| Theorem | neq0 4352* | A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | n0 4353* | A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | nel0 4354* | From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ | ||
| Theorem | reximdva0 4355* | Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓) | ||
| Theorem | rspn0 4356* | Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2141, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
| Theorem | n0rex 4357* | There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.) |
| ⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴) | ||
| Theorem | ssn0rex 4358* | There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐵 𝑥 ∈ 𝐴) | ||
| Theorem | n0moeu 4359* | A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.) |
| ⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) | ||
| Theorem | rex0 4360 | Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.) |
| ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 | ||
| Theorem | reu0 4361 | Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023.) |
| ⊢ ¬ ∃!𝑥 ∈ ∅ 𝜑 | ||
| Theorem | rmo0 4362 | Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023.) |
| ⊢ ∃*𝑥 ∈ ∅ 𝜑 | ||
| Theorem | 0el 4363* | Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.) |
| ⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
| Theorem | n0el 4364* | Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
| ⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥) | ||
| Theorem | eqeuel 4365* | A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.) |
| ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | ssdif0 4366 | Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) | ||
| Theorem | difn0 4367 | If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
| ⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵) | ||
| Theorem | pssdifn0 4368 | A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅) | ||
| Theorem | pssdif 4369 | A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | ||
| Theorem | ndisj 4370* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
| ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
| Theorem | inn0f 4371 | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
| Theorem | inn0 4372* | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
| Theorem | difin0ss 4373 | Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
| ⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵)) | ||
| Theorem | inssdif0 4374 | 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 | inindif 4375 | The intersection and class difference of a class with another class are disjoint. With inundif 4479, this shows that such intersection and class difference partition the class 𝐴. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
| ⊢ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅ | ||
| Theorem | difid 4376 | 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.) (Revised by David Abernethy, 17-Jun-2012.) |
| ⊢ (𝐴 ∖ 𝐴) = ∅ | ||
| Theorem | difidALT 4377 | Alternate proof of difid 4376. Shorter, but requiring ax-8 2110, df-clel 2816. (Contributed by NM, 22-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∖ 𝐴) = ∅ | ||
| Theorem | dif0 4378 | 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 | ab0w 4379* | The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 4380 using implicit substitution, which requires fewer axioms. (Contributed by GG, 3-Oct-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ 𝜓) | ||
| Theorem | ab0 4380 | The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 4385 (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 2941). (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.) (Proof shortened by SN, 8-Sep-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
| Theorem | ab0ALT 4381 | Alternate proof of ab0 4380, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
| Theorem | dfnf5 4382 | Characterization of nonfreeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.) |
| ⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)) | ||
| Theorem | ab0orv 4383* | The class abstraction defined by a formula 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.) Reduce axiom usage. (Revised by GG, 30-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅) | ||
| Theorem | ab0orvALT 4384* | Alternate proof of ab0orv 4383, shorter but using more axioms. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅) | ||
| Theorem | abn0 4385 | Nonempty class abstraction. See also ab0 4380. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.) |
| ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) | ||
| Theorem | rab0 4386 | 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 | rabeq0w 4387* | Condition for a restricted class abstraction to be empty. Version of rabeq0 4388 using implicit substitution, which does not require ax-10 2141, ax-11 2157, ax-12 2177, but requires ax-8 2110. (Contributed by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | ||
| Theorem | rabeq0 4388 | Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
| Theorem | rabn0 4389 | Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | rabxm 4390* | Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
| ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) | ||
| Theorem | rabnc 4391 | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ | ||
| Theorem | elneldisj 4392* | The set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.) |
| ⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶} ⇒ ⊢ (𝐸 ∩ 𝑁) = ∅ | ||
| Theorem | elnelun 4393* | The union of the set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 not containing the special element yields the original set. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.) |
| ⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶} ⇒ ⊢ (𝐸 ∪ 𝑁) = 𝐴 | ||
| Theorem | un0 4394 | 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 4395 | 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 | 0un 4396 | The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (∅ ∪ 𝐴) = 𝐴 | ||
| Theorem | 0in 4397 | The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (∅ ∩ 𝐴) = ∅ | ||
| Theorem | inv1 4398 | 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 4399 | 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 4400 | The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.) |
| ⊢ ∅ ⊆ 𝐴 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |