Definition df-n0 11899

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 11898	. 2 class ℕ0
2		cn 11638	. . 3 class ℕ
3		cc0 10537	. . . 4 class 0
4	3	csn 4567	. . 3 class {0}
5	2, 4	cun 3934	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1537	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  11900  nnssnn0  11901  nn0ssre  11902  nn0sscn  11903  nn0ex  11904  dfn2  11911  nn0addcl  11933  nn0mulcl  11934  nn0ssz  12004  dvdsprmpweqnn  16221  cply1coe0bi  20468  m2cpminvid2lem  21362  pmatcollpw3fi1  21396  dfrtrcl4  40132  corcltrcl  40133  cotrclrcl  40136