Theorem nnssnn0 12394

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 4129	. 2 ⊢ ℕ ⊆ (ℕ ∪ {0})
2		df-n0 12392	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
3	1, 2	sseqtrri 3981	1 ⊢ ℕ ⊆ ℕ0

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4577  0cc0 11016  ℕcn 12135  ℕ₀cn0 12391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-un 3904  df-ss 3916  df-n0 12392

This theorem is referenced by:  nnnn0  12398  nnnn0d  12452  nthruz  16172  oddge22np1  16270  bitsfzolem  16355  lcmfval  16542  ramub1  16950  ramcl  16951  ply1divex  26079  pserdvlem2  26375  2sqreunnlem1  27397  2sqreunnlem2  27403  fsum2dsub  34631  breprexplemc  34656  breprexpnat  34658  knoppndvlem18  36584  sumcubes  42421  hbtlem5  43235  brfvtrcld  43828  corcltrcl  43846  fourierdlem50  46268  fourierdlem102  46320  fourierdlem114  46332  fmtnoinf  47650  fmtnofac2  47683