Definition df-n0 11751

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 11750	. 2 class ℕ0
2		cn 11491	. . 3 class ℕ
3		cc0 10388	. . . 4 class 0
4	3	csn 4476	. . 3 class {0}
5	2, 4	cun 3861	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1522	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  11752  nnssnn0  11753  nn0ssre  11754  nn0sscn  11755  nn0ex  11756  dfn2  11763  nn0addcl  11785  nn0mulcl  11786  nn0ssz  11857  dvdsprmpweqnn  16055  cply1coe0bi  20156  m2cpminvid2lem  21051  pmatcollpw3fi1  21085  dfrtrcl4  39593  corcltrcl  39594  cotrclrcl  39597