Definition df-n0 12631

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 12630	. 2 class ℕ0
2		cn 12359	. . 3 class ℕ
3		cc0 11224	. . . 4 class 0
4	3	csn 4588	. . 3 class {0}
5	2, 4	cun 4152	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1570	1 wff ℕ0 = (ℕ ∪ {0})

This definition is used by:  elnn0  12632  nnssnn0  12633  nn0ssre  12634  nn0sscn  12635  nn0ex  12636  dfn2  12643  nn0addcl  12665  nn0mulcl  12666  nn0ssz  12740  dvdsprmpweqnn  17089  cply1coe0bi  22647  m2cpminvid2lem  23099  pmatcollpw3fi1  23133  dfrtrcl4  44928  corcltrcl  44929  cotrclrcl  44932