| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eq0 | Structured version Visualization version GIF version | ||
| Description: 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.) |
| Ref | Expression |
|---|---|
| eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfnul4 4335 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
| 2 | 1 | eqeq2i 2750 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
| 3 | dfcleq 2730 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
| 4 | df-clab 2715 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
| 5 | sbv 2088 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
| 6 | 4, 5 | bitri 275 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
| 7 | 6 | bibi2i 337 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
| 8 | nbfal 1555 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
| 9 | 7, 8 | bitr4i 278 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴) |
| 10 | 9 | albii 1819 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| 11 | 3, 10 | bitri 275 | . 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| 12 | 2, 11 | bitri 275 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1538 = wceq 1540 ⊥wfal 1552 [wsb 2064 ∈ wcel 2108 {cab 2714 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: neq0 4352 nel0 4354 0el 4363 ssdif0 4366 difin0ss 4373 inssdif0 4374 disjiun 5131 0ex 5307 reldm0 5938 iresn0n0 6072 uzwo 12953 hashgt0elex 14440 nrhmzr 20537 zrninitoringc 20676 hausdiag 23653 rnelfmlem 23960 elons2 28281 prv0 35435 wzel 35825 knoppndv 36535 bj-nul 37057 bj-nuliota 37058 bj-nuliotaALT 37059 nninfnub 37758 prtlem14 38875 orddif0suc 43281 |
| Copyright terms: Public domain | W3C validator |