Theorem nnssnn0 12502

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4589  0cc0 11095  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-n0 12500

This theorem is referenced by:  nnnn0  12506  nnnn0d  12560  nthruz  16304  oddge22np1  16402  bitsfzolem  16487  lcmfval  16674  ramub1  17083  ramcl  17084  ply1divex  26294  pserdvlem2  26591  2sqreunnlem1  27613  2sqreunnlem2  27619  fsum2dsub  34994  breprexplemc  35019  breprexpnat  35021  knoppndvlem18  37118  sumcubes  43074  hbtlem5  43855  brfvtrcld  44447  corcltrcl  44465  fourierdlem50  46870  fourierdlem102  46922  fourierdlem114  46934  fmtnoinf  48288  fmtnofac2  48321