Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnssnn0 Structured version   Visualization version   GIF version

Theorem nnssnn0 11891
 Description: Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
nnssnn0 ℕ ⊆ ℕ0

Proof of Theorem nnssnn0
StepHypRef Expression
1 ssun1 4099 . 2 ℕ ⊆ (ℕ ∪ {0})
2 df-n0 11889 . 2 0 = (ℕ ∪ {0})
31, 2sseqtrri 3952 1 ℕ ⊆ ℕ0
 Colors of variables: wff setvar class Syntax hints:   ∪ cun 3879   ⊆ wss 3881  {csn 4525  0cc0 10529  ℕcn 11628  ℕ0cn0 11888 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-n0 11889 This theorem is referenced by:  nnnn0  11895  nnnn0d  11946  nthruz  15601  oddge22np1  15693  bitsfzolem  15776  lcmfval  15958  ramub1  16357  ramcl  16358  ply1divex  24747  pserdvlem2  25033  2sqreunnlem1  26043  2sqreunnlem2  26049  fsum2dsub  32003  breprexplemc  32028  breprexpnat  32030  knoppndvlem18  33996  hbtlem5  40115  brfvtrcld  40465  corcltrcl  40483  fourierdlem50  42841  fourierdlem102  42893  fourierdlem114  42905  fmtnoinf  44096  fmtnofac2  44129
 Copyright terms: Public domain W3C validator