Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eq0 | Structured version Visualization version GIF version |
Description: The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
eq0 | ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2764 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | eq0f 3925 | 1 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∀wal 1481 = wceq 1483 ∈ wcel 1990 ∅c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: nel0 3932 0el 3939 ssdif0 3942 difin0ss 3946 inssdif0 3947 ralf0 4078 ralf0OLD 4079 disjiun 4640 0ex 4790 reldm0 5343 uzwo 11751 hashgt0elex 13189 hausdiag 21448 rnelfmlem 21756 wzel 31771 wzelOLD 31772 unblimceq0 32498 knoppndv 32525 bj-ab0 32902 bj-nul 33018 bj-nuliota 33019 bj-nuliotaALT 33020 nninfnub 33547 prtlem14 34159 nrhmzr 41873 zrninitoringc 42071 |
Copyright terms: Public domain | W3C validator |