Theorem nnssnn0 12416

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4582  0cc0 11038  ℕcn 12157  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-n0 12414

This theorem is referenced by:  nnnn0  12420  nnnn0d  12474  nthruz  16190  oddge22np1  16288  bitsfzolem  16373  lcmfval  16560  ramub1  16968  ramcl  16969  ply1divex  26110  pserdvlem2  26406  2sqreunnlem1  27428  2sqreunnlem2  27434  fsum2dsub  34785  breprexplemc  34810  breprexpnat  34812  knoppndvlem18  36751  sumcubes  42683  hbtlem5  43485  brfvtrcld  44077  corcltrcl  44095  fourierdlem50  46514  fourierdlem102  46566  fourierdlem114  46578  fmtnoinf  47896  fmtnofac2  47929