Theorem nnssnn0 12431

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4555  0cc0 11029  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-n0 12429

This theorem is referenced by:  nnnn0  12435  nnnn0d  12489  nthruz  16211  oddge22np1  16309  bitsfzolem  16394  lcmfval  16581  ramub1  16990  ramcl  16991  ply1divex  26120  pserdvlem2  26411  2sqreunnlem1  27430  2sqreunnlem2  27436  fsum2dsub  34791  breprexplemc  34816  breprexpnat  34818  knoppndvlem18  36835  sumcubes  42790  hbtlem5  43573  brfvtrcld  44165  corcltrcl  44183  fourierdlem50  46599  fourierdlem102  46651  fourierdlem114  46663  fmtnoinf  48014  fmtnofac2  48047