MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-n0 Structured version   Visualization version   GIF version

Definition df-n0 11331
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
StepHypRef Expression
1 cn0 11330 . 2 class 0
2 cn 11058 . . 3 class
3 cc0 9974 . . . 4 class 0
43csn 4210 . . 3 class {0}
52, 4cun 3605 . 2 class (ℕ ∪ {0})
61, 5wceq 1523 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11332  nnssnn0  11333  nn0ssre  11334  nn0ex  11336  dfn2  11343  nn0addcl  11366  nn0mulcl  11367  nn0ssz  11436  dvdsprmpweqnn  15636  cply1coe0bi  19718  m2cpminvid2lem  20607  pmatcollpw3fi1  20641  dfrtrcl4  38347  corcltrcl  38348  cotrclrcl  38351
  Copyright terms: Public domain W3C validator