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 11887
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 11886 . 2 class 0
2 cn 11627 . . 3 class
3 cc0 10526 . . . 4 class 0
43csn 4559 . . 3 class {0}
52, 4cun 3933 . 2 class (ℕ ∪ {0})
61, 5wceq 1528 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11888  nnssnn0  11889  nn0ssre  11890  nn0sscn  11891  nn0ex  11892  dfn2  11899  nn0addcl  11921  nn0mulcl  11922  nn0ssz  11992  dvdsprmpweqnn  16211  cply1coe0bi  20398  m2cpminvid2lem  21292  pmatcollpw3fi1  21326  dfrtrcl4  39963  corcltrcl  39964  cotrclrcl  39967
  Copyright terms: Public domain W3C validator