![]() |
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.) |
Ref | Expression |
---|---|
eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2932 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | eq0f 4191 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∀wal 1505 = wceq 1507 ∈ wcel 2050 ∅c0 4178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-dif 3832 df-nul 4179 |
This theorem is referenced by: nel0 4197 0el 4206 ssdif0 4209 difin0ss 4214 inssdif0 4215 ralf0 4340 disjiun 4917 0ex 5068 reldm0 5641 uzwo 12125 hashgt0elex 13575 hausdiag 21957 rnelfmlem 22264 wzel 32638 knoppndv 33399 bj-ab0 33722 bj-nul 33866 bj-nuliota 33867 bj-nuliotaALT 33868 nninfnub 34474 prtlem14 35461 nrhmzr 43514 zrninitoringc 43712 |
Copyright terms: Public domain | W3C validator |