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 2160, ax-12 2177. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2114, df-clel 2809. (Revised by Gino Giotto, 6-Sep-2024.) |
Ref | Expression |
---|---|
eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnul4 4225 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
2 | 1 | eqeq2i 2749 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
3 | dfcleq 2729 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
4 | df-clab 2715 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
5 | sbv 2096 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
6 | 4, 5 | bitri 278 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
7 | 6 | bibi2i 341 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
8 | nbfal 1558 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
9 | 7, 8 | bitr4i 281 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ¬ 𝑥 ∈ 𝐴) |
10 | 9 | albii 1827 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
11 | 3, 10 | bitri 278 | . 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
12 | 2, 11 | bitri 278 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∀wal 1541 = wceq 1543 ⊥wfal 1555 [wsb 2072 ∈ wcel 2112 {cab 2714 ∅c0 4223 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-dif 3856 df-nul 4224 |
This theorem is referenced by: neq0 4246 nel0 4251 0el 4261 ssdif0 4264 difin0ss 4269 inssdif0 4270 ralf0OLD 4415 disjiun 5026 0ex 5185 reldm0 5782 iresn0n0 5908 uzwo 12472 hashgt0elex 13933 hausdiag 22496 rnelfmlem 22803 prv0 33059 wzel 33498 knoppndv 34400 bj-nul 34913 bj-nuliota 34914 bj-nuliotaALT 34915 nninfnub 35595 prtlem14 36574 nrhmzr 45047 zrninitoringc 45245 |
Copyright terms: Public domain | W3C validator |