Definition df-n0 12511

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 12510	. 2 class ℕ0
2		cn 12239	. . 3 class ℕ
3		cc0 11106	. . . 4 class 0
4	3	csn 4588	. . 3 class {0}
5	2, 4	cun 3902	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1569	1 wff ℕ0 = (ℕ ∪ {0})

This definition is used by:  elnn0  12512  nnssnn0  12513  nn0ssre  12514  nn0sscn  12515  nn0ex  12516  dfn2  12523  nn0addcl  12545  nn0mulcl  12546  nn0ssz  12620  dvdsprmpweqnn  16951  cply1coe0bi  22473  m2cpminvid2lem  22922  pmatcollpw3fi1  22956  dfrtrcl4  44492  corcltrcl  44493  cotrclrcl  44496