Theorem nnssnn0 12504

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

Syntax hints:   ∪ cun 3924   ⊆ wss 3926  {csn 4601  0cc0 11129  ℕcn 12240  ℕ₀cn0 12501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-n0 12502

This theorem is referenced by:  nnnn0  12508  nnnn0d  12562  nthruz  16271  oddge22np1  16368  bitsfzolem  16453  lcmfval  16640  ramub1  17048  ramcl  17049  ply1divex  26094  pserdvlem2  26390  2sqreunnlem1  27412  2sqreunnlem2  27418  fsum2dsub  34639  breprexplemc  34664  breprexpnat  34666  knoppndvlem18  36547  sumcubes  42362  hbtlem5  43152  brfvtrcld  43745  corcltrcl  43763  fourierdlem50  46185  fourierdlem102  46237  fourierdlem114  46249  fmtnoinf  47550  fmtnofac2  47583