Definition df-n0 12443

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 12442	. 2 class ℕ0
2		cn 12186	. . 3 class ℕ
3		cc0 11068	. . . 4 class 0
4	3	csn 4589	. . 3 class {0}
5	2, 4	cun 3912	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12444  nnssnn0  12445  nn0ssre  12446  nn0sscn  12447  nn0ex  12448  dfn2  12455  nn0addcl  12477  nn0mulcl  12478  nn0ssz  12552  dvdsprmpweqnn  16856  cply1coe0bi  22189  m2cpminvid2lem  22641  pmatcollpw3fi1  22675  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731