This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0ex

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 . (Contributed by NM, 21-Jun-1993) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion 0ex ⊢ ∅ ∈ V

Proof

Step Hyp Ref Expression
1 ax-nul ⊢ ∃ x ∀ y ¬ y ∈ x
2 eq0 ⊢ x = ∅ ↔ ∀ y ¬ y ∈ x
3 2 exbii ⊢ ∃ x x = ∅ ↔ ∃ x ∀ y ¬ y ∈ x
4 1 3 mpbir ⊢ ∃ x x = ∅
5 4 issetri ⊢ ∅ ∈ V