Theorem nnssnn0 12166

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4558  0cc0 10802  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-n0 12164

This theorem is referenced by:  nnnn0  12170  nnnn0d  12223  nthruz  15890  oddge22np1  15986  bitsfzolem  16069  lcmfval  16254  ramub1  16657  ramcl  16658  ply1divex  25206  pserdvlem2  25492  2sqreunnlem1  26502  2sqreunnlem2  26508  fsum2dsub  32487  breprexplemc  32512  breprexpnat  32514  knoppndvlem18  34636  hbtlem5  40869  brfvtrcld  41218  corcltrcl  41236  fourierdlem50  43587  fourierdlem102  43639  fourierdlem114  43651  fmtnoinf  44876  fmtnofac2  44909