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 2975 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | eq0f 4303 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ∀wal 1529 = wceq 1531 ∈ wcel 2108 ∅c0 4289 |
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 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-dif 3937 df-nul 4290 |
This theorem is referenced by: nel0 4309 0el 4318 ssdif0 4321 difin0ss 4326 inssdif0 4327 ralf0 4455 disjiun 5044 0ex 5202 reldm0 5791 iresn0n0 5916 uzwo 12303 hashgt0elex 13754 hausdiag 22245 rnelfmlem 22552 prv0 32670 wzel 33104 knoppndv 33866 bj-ab0 34217 bj-nul 34341 bj-nuliota 34342 bj-nuliotaALT 34343 nninfnub 35018 prtlem14 36002 nrhmzr 44135 zrninitoringc 44333 |
Copyright terms: Public domain | W3C validator |