Definition df-n0 12385

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 12384	. 2 class ℕ0
2		cn 12128	. . 3 class ℕ
3		cc0 11009	. . . 4 class 0
4	3	csn 4577	. . 3 class {0}
5	2, 4	cun 3901	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12386  nnssnn0  12387  nn0ssre  12388  nn0sscn  12389  nn0ex  12390  dfn2  12397  nn0addcl  12419  nn0mulcl  12420  nn0ssz  12494  dvdsprmpweqnn  16797  cply1coe0bi  22187  m2cpminvid2lem  22639  pmatcollpw3fi1  22673  dfrtrcl4  43721  corcltrcl  43722  cotrclrcl  43725