Definition df-n0 12379

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 12378	. 2 class ℕ0
2		cn 12122	. . 3 class ℕ
3		cc0 11003	. . . 4 class 0
4	3	csn 4576	. . 3 class {0}
5	2, 4	cun 3900	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1541	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12380  nnssnn0  12381  nn0ssre  12382  nn0sscn  12383  nn0ex  12384  dfn2  12391  nn0addcl  12413  nn0mulcl  12414  nn0ssz  12488  dvdsprmpweqnn  16794  cply1coe0bi  22215  m2cpminvid2lem  22667  pmatcollpw3fi1  22701  dfrtrcl4  43770  corcltrcl  43771  cotrclrcl  43774