Theorem nnssnn0 12479

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

Syntax hints:   ∪ cun 3945   ⊆ wss 3947  {csn 4627  0cc0 11112  ℕcn 12216  ℕ₀cn0 12476

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-n0 12477

This theorem is referenced by:  nnnn0  12483  nnnn0d  12536  nthruz  16200  oddge22np1  16296  bitsfzolem  16379  lcmfval  16562  ramub1  16965  ramcl  16966  ply1divex  25889  pserdvlem2  26176  2sqreunnlem1  27188  2sqreunnlem2  27194  fsum2dsub  33917  breprexplemc  33942  breprexpnat  33944  knoppndvlem18  35708  sumcubes  41513  hbtlem5  42172  brfvtrcld  42774  corcltrcl  42792  fourierdlem50  45170  fourierdlem102  45222  fourierdlem114  45234  fmtnoinf  46502  fmtnofac2  46535