Definition df-n0 12532

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 12531	. 2 class ℕ0
2		cn 12260	. . 3 class ℕ
3		cc0 11127	. . . 4 class 0
4	3	csn 4587	. . 3 class {0}
5	2, 4	cun 3900	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1570	1 wff ℕ0 = (ℕ ∪ {0})

This definition is used by:  elnn0  12533  nnssnn0  12534  nn0ssre  12535  nn0sscn  12536  nn0ex  12537  dfn2  12544  nn0addcl  12566  nn0mulcl  12567  nn0ssz  12641  dvdsprmpweqnn  16981  cply1coe0bi  22528  m2cpminvid2lem  22980  pmatcollpw3fi1  23014  dfrtrcl4  44565  corcltrcl  44566  cotrclrcl  44569