Definition df-n0 12416

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

Assertion

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

Detailed syntax breakdown of Definition df-n0

Step	Hyp	Ref	Expression
1		cn0 12415	. 2 class ℕ0
2		cn 12159	. . 3 class ℕ
3		cc0 11040	. . . 4 class 0
4	3	csn 4582	. . 3 class {0}
5	2, 4	cun 3901	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1542	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12417  nnssnn0  12418  nn0ssre  12419  nn0sscn  12420  nn0ex  12421  dfn2  12428  nn0addcl  12450  nn0mulcl  12451  nn0ssz  12525  dvdsprmpweqnn  16827  cply1coe0bi  22263  m2cpminvid2lem  22715  pmatcollpw3fi1  22749  dfrtrcl4  44123  corcltrcl  44124  cotrclrcl  44127