![]() |
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 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.) |
Ref | Expression |
---|---|
eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnul4 4340 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
2 | 1 | eqeq2i 2747 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
3 | dfcleq 2727 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
4 | df-clab 2712 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
5 | sbv 2085 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
6 | 4, 5 | bitri 275 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
7 | 6 | bibi2i 337 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
8 | nbfal 1551 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
9 | 7, 8 | bitr4i 278 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴) |
10 | 9 | albii 1815 | . . 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 1534 = wceq 1536 ⊥wfal 1548 [wsb 2061 ∈ wcel 2105 {cab 2711 ∅c0 4338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-dif 3965 df-nul 4339 |
This theorem is referenced by: neq0 4357 nel0 4359 0el 4368 ssdif0 4371 difin0ss 4378 inssdif0 4379 disjiun 5135 0ex 5312 reldm0 5940 iresn0n0 6073 uzwo 12950 hashgt0elex 14436 nrhmzr 20553 zrninitoringc 20692 hausdiag 23668 rnelfmlem 23975 elons2 28295 prv0 35414 wzel 35805 knoppndv 36516 bj-nul 37038 bj-nuliota 37039 bj-nuliotaALT 37040 nninfnub 37737 prtlem14 38855 orddif0suc 43257 |
Copyright terms: Public domain | W3C validator |