Theorem nnssnn0 12474

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

Syntax hints:   ∪ cun 3946   ⊆ wss 3948  {csn 4628  0cc0 11109  ℕcn 12211  ℕ₀cn0 12471

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-n0 12472

This theorem is referenced by:  nnnn0  12478  nnnn0d  12531  nthruz  16195  oddge22np1  16291  bitsfzolem  16374  lcmfval  16557  ramub1  16960  ramcl  16961  ply1divex  25653  pserdvlem2  25939  2sqreunnlem1  26949  2sqreunnlem2  26955  fsum2dsub  33614  breprexplemc  33639  breprexpnat  33641  knoppndvlem18  35400  sumcubes  41211  hbtlem5  41860  brfvtrcld  42462  corcltrcl  42480  fourierdlem50  44862  fourierdlem102  44914  fourierdlem114  44926  fmtnoinf  46194  fmtnofac2  46227