Theorem nnssnn0 12236

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

Step	Hyp	Ref	Expression
1		ssun1 4106	. 2 ⊢ ℕ ⊆ (ℕ ∪ {0})
2		df-n0 12234	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
3	1, 2	sseqtrri 3958	1 ⊢ ℕ ⊆ ℕ0

Syntax hints:   ∪ cun 3885   ⊆ wss 3887  {csn 4561  0cc0 10871  ℕcn 11973  ℕ₀cn0 12233

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-n0 12234

This theorem is referenced by:  nnnn0  12240  nnnn0d  12293  nthruz  15962  oddge22np1  16058  bitsfzolem  16141  lcmfval  16326  ramub1  16729  ramcl  16730  ply1divex  25301  pserdvlem2  25587  2sqreunnlem1  26597  2sqreunnlem2  26603  fsum2dsub  32587  breprexplemc  32612  breprexpnat  32614  knoppndvlem18  34709  hbtlem5  40953  brfvtrcld  41329  corcltrcl  41347  fourierdlem50  43697  fourierdlem102  43749  fourierdlem114  43761  fmtnoinf  44988  fmtnofac2  45021