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 11170
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 11169 . 2 class 0
2 cn 10897 . . 3 class
3 cc0 9815 . . . 4 class 0
43csn 4125 . . 3 class {0}
52, 4cun 3538 . 2 class (ℕ ∪ {0})
61, 5wceq 1475 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11171  nnssnn0  11172  nn0ssre  11173  nn0ex  11175  dfn2  11182  nn0addcl  11205  nn0mulcl  11206  nn0ssz  11275  dvdsprmpweqnn  15427  cply1coe0bi  19491  m2cpminvid2lem  20378  pmatcollpw3fi1  20412  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053
  Copyright terms: Public domain W3C validator