Theorem nnssnn0 12395

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

Syntax hints:   ∪ cun 3896   ⊆ wss 3898  {csn 4577  0cc0 11017  ℕcn 12136  ℕ₀cn0 12392

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 3439  df-un 3903  df-ss 3915  df-n0 12393

This theorem is referenced by:  nnnn0  12399  nnnn0d  12453  nthruz  16169  oddge22np1  16267  bitsfzolem  16352  lcmfval  16539  ramub1  16947  ramcl  16948  ply1divex  26089  pserdvlem2  26385  2sqreunnlem1  27407  2sqreunnlem2  27413  fsum2dsub  34692  breprexplemc  34717  breprexpnat  34719  knoppndvlem18  36645  sumcubes  42483  hbtlem5  43285  brfvtrcld  43878  corcltrcl  43896  fourierdlem50  46316  fourierdlem102  46368  fourierdlem114  46380  fmtnoinf  47698  fmtnofac2  47731