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

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {csn 4568  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  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  26112  pserdvlem2  26406  2sqreunnlem1  27426  2sqreunnlem2  27432  fsum2dsub  34767  breprexplemc  34792  breprexpnat  34794  knoppndvlem18  36805  sumcubes  42759  hbtlem5  43574  brfvtrcld  44166  corcltrcl  44184  fourierdlem50  46602  fourierdlem102  46654  fourierdlem114  46666  fmtnoinf  48011  fmtnofac2  48044