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

Theorem nnssnn0 11142
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 3737 . 2 ℕ ⊆ (ℕ ∪ {0})
2 df-n0 11140 . 2 0 = (ℕ ∪ {0})
31, 2sseqtr4i 3600 1 ℕ ⊆ ℕ0
Colors of variables: wff setvar class
Syntax hints:  cun 3537  wss 3539  {csn 4124  0cc0 9792  cn 10867  0cn0 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553  df-n0 11140
This theorem is referenced by:  nnnn0  11146  nnnn0d  11198  nthruz  14766  oddge22np1  14857  bitsfzolem  14940  lcmfval  15118  ramub1  15516  ramcl  15517  ply1divex  23617  pserdvlem2  23903  knoppndvlem18  31496  hbtlem5  36520  brfvtrcld  36835  corcltrcl  36853  fourierdlem50  38853  fourierdlem102  38905  fourierdlem114  38917  fmtnoinf  39791  fmtnofac2  39824
  Copyright terms: Public domain W3C validator