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