Definition df-n0

Description: Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cn0	⊢ ℕ0
1		cn	⊢ ℕ
2		cc0	⊢ 0
3	2	csn	⊢ { 0 }
4	1 3	cun	⊢ ( ℕ ∪ { 0 } )
5	0 4	wceq	⊢ ℕ0 = ( ℕ ∪ { 0 } )