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