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 11485
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 11484 . 2 class 0
2 cn 11212 . . 3 class
3 cc0 10128 . . . 4 class 0
43csn 4321 . . 3 class {0}
52, 4cun 3713 . 2 class (ℕ ∪ {0})
61, 5wceq 1632 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11486  nnssnn0  11487  nn0ssre  11488  nn0ex  11490  dfn2  11497  nn0addcl  11520  nn0mulcl  11521  nn0ssz  11590  dvdsprmpweqnn  15791  cply1coe0bi  19872  m2cpminvid2lem  20761  pmatcollpw3fi1  20795  dfrtrcl4  38532  corcltrcl  38533  cotrclrcl  38536
  Copyright terms: Public domain W3C validator