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 11142
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 11141 . 2 class 0
2 cn 10869 . . 3 class
3 cc0 9792 . . . 4 class 0
43csn 4124 . . 3 class {0}
52, 4cun 3537 . 2 class (ℕ ∪ {0})
61, 5wceq 1474 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11143  nnssnn0  11144  nn0ssre  11145  nn0ex  11147  dfn2  11154  nn0addcl  11177  nn0mulcl  11178  nn0ssz  11233  dvdsprmpweqnn  15375  cply1coe0bi  19439  m2cpminvid2lem  20325  pmatcollpw3fi1  20359  dfrtrcl4  36832  corcltrcl  36833  cotrclrcl  36836
  Copyright terms: Public domain W3C validator