Theorem nnssnn0 12478

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

Syntax hints:   ∪ cun 3900   ⊆ wss 3902  {csn 4579  0cc0 11067  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-n0 12476

This theorem is referenced by:  nnnn0  12482  nnnn0d  12536  nthruz  16276  oddge22np1  16374  bitsfzolem  16459  lcmfval  16646  ramub1  17055  ramcl  17056  ply1divex  26185  pserdvlem2  26479  2sqreunnlem1  27501  2sqreunnlem2  27507  fsum2dsub  34862  breprexplemc  34887  breprexpnat  34889  knoppndvlem18  36928  sumcubes  42883  hbtlem5  43666  brfvtrcld  44258  corcltrcl  44276  fourierdlem50  46691  fourierdlem102  46743  fourierdlem114  46755  fmtnoinf  48106  fmtnofac2  48139