Definition df-n0 12403

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 12402	. 2 class ℕ0
2		cn 12146	. . 3 class ℕ
3		cc0 11028	. . . 4 class 0
4	3	csn 4579	. . 3 class {0}
5	2, 4	cun 3903	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12404  nnssnn0  12405  nn0ssre  12406  nn0sscn  12407  nn0ex  12408  dfn2  12415  nn0addcl  12437  nn0mulcl  12438  nn0ssz  12512  dvdsprmpweqnn  16815  cply1coe0bi  22205  m2cpminvid2lem  22657  pmatcollpw3fi1  22691  dfrtrcl4  43711  corcltrcl  43712  cotrclrcl  43715