Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ex | Structured version Visualization version GIF version |
Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 5233. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
0ex | ⊢ ∅ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-nul 5233 | . . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | |
2 | eq0 4280 | . . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥) | |
3 | 2 | exbii 1846 | . . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) |
4 | 1, 3 | mpbir 230 | . 2 ⊢ ∃𝑥 𝑥 = ∅ |
5 | 4 | issetri 3450 | 1 ⊢ ∅ ∈ V |
Copyright terms: Public domain | W3C validator |