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

Metamath Proof Explorer

Theorem nn0ex

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004)

Ref Expression
Assertion nn0ex ⊢ ℕ 0 ∈ V

Proof

Step Hyp Ref Expression
1 df-n0 ⊢ ℕ 0 = ℕ ∪ 0
2 nnex ⊢ ℕ ∈ V
3 snex ⊢ 0 ∈ V
4 2 3 unex ⊢ ℕ ∪ 0 ∈ V
5 1 4 eqeltri ⊢ ℕ 0 ∈ V