Definition df-n0 12056

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 12055	. 2 class ℕ0
2		cn 11795	. . 3 class ℕ
3		cc0 10694	. . . 4 class 0
4	3	csn 4527	. . 3 class {0}
5	2, 4	cun 3851	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1543	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12057  nnssnn0  12058  nn0ssre  12059  nn0sscn  12060  nn0ex  12061  dfn2  12068  nn0addcl  12090  nn0mulcl  12091  nn0ssz  12163  dvdsprmpweqnn  16401  cply1coe0bi  21175  m2cpminvid2lem  21605  pmatcollpw3fi1  21639  dfrtrcl4  40964  corcltrcl  40965  cotrclrcl  40968