Theorem nnssnn0 12379

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

Syntax hints:   ∪ cun 3895   ⊆ wss 3897  {csn 4571  0cc0 11001  ℕcn 12120  ℕ₀cn0 12376

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-n0 12377

This theorem is referenced by:  nnnn0  12383  nnnn0d  12437  nthruz  16157  oddge22np1  16255  bitsfzolem  16340  lcmfval  16527  ramub1  16935  ramcl  16936  ply1divex  26064  pserdvlem2  26360  2sqreunnlem1  27382  2sqreunnlem2  27388  fsum2dsub  34612  breprexplemc  34637  breprexpnat  34639  knoppndvlem18  36563  sumcubes  42346  hbtlem5  43161  brfvtrcld  43754  corcltrcl  43772  fourierdlem50  46194  fourierdlem102  46246  fourierdlem114  46258  fmtnoinf  47567  fmtnofac2  47600