Theorem nnssnn0 12556

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

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {csn 4648  0cc0 11184  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-n0 12554

This theorem is referenced by:  nnnn0  12560  nnnn0d  12613  nthruz  16301  oddge22np1  16397  bitsfzolem  16480  lcmfval  16668  ramub1  17075  ramcl  17076  ply1divex  26196  pserdvlem2  26490  2sqreunnlem1  27511  2sqreunnlem2  27517  fsum2dsub  34584  breprexplemc  34609  breprexpnat  34611  knoppndvlem18  36495  sumcubes  42301  hbtlem5  43085  brfvtrcld  43683  corcltrcl  43701  fourierdlem50  46077  fourierdlem102  46129  fourierdlem114  46141  fmtnoinf  47410  fmtnofac2  47443