![]() |
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 2147, ax-12 2167. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2101, df-clel 2803. (Revised by GG, 6-Sep-2024.) |
Ref | Expression |
---|---|
eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnul4 4326 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
2 | 1 | eqeq2i 2739 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
3 | dfcleq 2719 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
4 | df-clab 2704 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
5 | sbv 2084 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
6 | 4, 5 | bitri 274 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
7 | 6 | bibi2i 336 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
8 | nbfal 1549 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
9 | 7, 8 | bitr4i 277 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴) |
10 | 9 | albii 1814 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
11 | 3, 10 | bitri 274 | . 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
12 | 2, 11 | bitri 274 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1532 = wceq 1534 ⊥wfal 1546 [wsb 2060 ∈ wcel 2099 {cab 2703 ∅c0 4324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-dif 3951 df-nul 4325 |
This theorem is referenced by: neq0 4347 nel0 4349 0el 4358 ssdif0 4361 difin0ss 4368 inssdif0 4369 ralf0OLD 4514 disjiun 5133 0ex 5304 reldm0 5926 iresn0n0 6055 uzwo 12940 hashgt0elex 14412 nrhmzr 20514 zrninitoringc 20649 hausdiag 23636 rnelfmlem 23943 elons2 28248 prv0 35270 wzel 35660 knoppndv 36249 bj-nul 36775 bj-nuliota 36776 bj-nuliotaALT 36777 nninfnub 37464 prtlem14 38584 orddif0suc 42970 |
Copyright terms: Public domain | W3C validator |