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 11563
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 11562 . 2 class 0
2 cn 11308 . . 3 class
3 cc0 10224 . . . 4 class 0
43csn 4377 . . 3 class {0}
52, 4cun 3774 . 2 class (ℕ ∪ {0})
61, 5wceq 1637 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11564  nnssnn0  11565  nn0ssre  11566  nn0ex  11568  dfn2  11575  nn0addcl  11597  nn0mulcl  11598  nn0ssz  11667  dvdsprmpweqnn  15809  cply1coe0bi  19881  m2cpminvid2lem  20776  pmatcollpw3fi1  20810  dfrtrcl4  38531  corcltrcl  38532  cotrclrcl  38535
  Copyright terms: Public domain W3C validator