Definition df-n0 12554

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 12553	. 2 class ℕ0
2		cn 12293	. . 3 class ℕ
3		cc0 11184	. . . 4 class 0
4	3	csn 4648	. . 3 class {0}
5	2, 4	cun 3974	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1537	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12555  nnssnn0  12556  nn0ssre  12557  nn0sscn  12558  nn0ex  12559  dfn2  12566  nn0addcl  12588  nn0mulcl  12589  nn0ssz  12662  dvdsprmpweqnn  16932  cply1coe0bi  22327  m2cpminvid2lem  22781  pmatcollpw3fi1  22815  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704