Theorem nnssnn0 12452

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

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  0cc0 11075  ℕcn 12193  ℕ₀cn0 12449

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-n0 12450

This theorem is referenced by:  nnnn0  12456  nnnn0d  12510  nthruz  16228  oddge22np1  16326  bitsfzolem  16411  lcmfval  16598  ramub1  17006  ramcl  17007  ply1divex  26049  pserdvlem2  26345  2sqreunnlem1  27367  2sqreunnlem2  27373  fsum2dsub  34605  breprexplemc  34630  breprexpnat  34632  knoppndvlem18  36524  sumcubes  42308  hbtlem5  43124  brfvtrcld  43717  corcltrcl  43735  fourierdlem50  46161  fourierdlem102  46213  fourierdlem114  46225  fmtnoinf  47541  fmtnofac2  47574