Theorem nnssnn0 12613

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

This proof depends on syntax axioms:   ⊆ wss 3895   ∪ cun 4149  {csn 4584  0cc0 11204  ℕcn 12339  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-n0 12611

This theorem is used by:  nnnn0  12617  nnnn0d  12671  nthruz  16427  oddge22np1  16525  bitsfzolem  16610  lcmfval  16802  ramub1  17212  ramcl  17213  ply1divex  26461  pserdvlem2  26761  2sqreunnlem1  27782  2sqreunnlem2  27788  fsum2dsub  35283  breprexplemc  35308  breprexpnat  35310  knoppndvlem18  37488  sumcubes  43464  hbtlem5  44224  brfvtrcld  44815  corcltrcl  44833  hfstructcan  46125  fourierdlem50  47260  fourierdlem102  47312  fourierdlem114  47324  fmtnoinf  48715  fmtnofac2  48748