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 11253
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 11252 . 2 class 0
2 cn 10980 . . 3 class
3 cc0 9896 . . . 4 class 0
43csn 4155 . . 3 class {0}
52, 4cun 3558 . 2 class (ℕ ∪ {0})
61, 5wceq 1480 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11254  nnssnn0  11255  nn0ssre  11256  nn0ex  11258  dfn2  11265  nn0addcl  11288  nn0mulcl  11289  nn0ssz  11358  dvdsprmpweqnn  15532  cply1coe0bi  19610  m2cpminvid2lem  20499  pmatcollpw3fi1  20533  dfrtrcl4  37550  corcltrcl  37551  cotrclrcl  37554
  Copyright terms: Public domain W3C validator