Definition df-n0 12433

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 12432	. 2 class ℕ0
2		cn 12169	. . 3 class ℕ
3		cc0 11034	. . . 4 class 0
4	3	csn 4557	. . 3 class {0}
5	2, 4	cun 3882	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1548	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12434  nnssnn0  12435  nn0ssre  12436  nn0sscn  12437  nn0ex  12438  dfn2  12445  nn0addcl  12467  nn0mulcl  12468  nn0ssz  12542  dvdsprmpweqnn  16851  cply1coe0bi  22291  m2cpminvid2lem  22740  pmatcollpw3fi1  22774  dfrtrcl4  44195  corcltrcl  44196  cotrclrcl  44199