Theorem nnssnn0 12527

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

Syntax hints:   ∪ cun 3961   ⊆ wss 3963  {csn 4631  0cc0 11153  ℕcn 12264  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-n0 12525

This theorem is referenced by:  nnnn0  12531  nnnn0d  12585  nthruz  16286  oddge22np1  16383  bitsfzolem  16468  lcmfval  16655  ramub1  17062  ramcl  17063  ply1divex  26191  pserdvlem2  26487  2sqreunnlem1  27508  2sqreunnlem2  27514  fsum2dsub  34601  breprexplemc  34626  breprexpnat  34628  knoppndvlem18  36512  sumcubes  42326  hbtlem5  43117  brfvtrcld  43711  corcltrcl  43729  fourierdlem50  46112  fourierdlem102  46164  fourierdlem114  46176  fmtnoinf  47461  fmtnofac2  47494