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

Theorem nnssnn0 12417
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 4133 . 2 ℕ ⊆ (ℕ ∪ {0})
2 df-n0 12415 . 2 0 = (ℕ ∪ {0})
31, 2sseqtrri 3982 1 ℕ ⊆ ℕ0
Colors of variables: wff setvar class
Syntax hints:  cun 3909  wss 3911  {csn 4587  0cc0 11052  cn 12154  0cn0 12414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-un 3916  df-in 3918  df-ss 3928  df-n0 12415
This theorem is referenced by:  nnnn0  12421  nnnn0d  12474  nthruz  16136  oddge22np1  16232  bitsfzolem  16315  lcmfval  16498  ramub1  16901  ramcl  16902  ply1divex  25504  pserdvlem2  25790  2sqreunnlem1  26800  2sqreunnlem2  26806  fsum2dsub  33223  breprexplemc  33248  breprexpnat  33250  knoppndvlem18  34995  hbtlem5  41458  brfvtrcld  42000  corcltrcl  42018  fourierdlem50  44404  fourierdlem102  44456  fourierdlem114  44468  fmtnoinf  45735  fmtnofac2  45768
  Copyright terms: Public domain W3C validator