Theorem nnssnn0 12503

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4591  0cc0 11096  ℕcn 12229  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-n0 12501

This theorem is referenced by:  nnnn0  12507  nnnn0d  12561  nthruz  16305  oddge22np1  16403  bitsfzolem  16488  lcmfval  16675  ramub1  17084  ramcl  17085  ply1divex  26259  pserdvlem2  26553  2sqreunnlem1  27575  2sqreunnlem2  27581  fsum2dsub  34935  breprexplemc  34960  breprexpnat  34962  knoppndvlem18  37003  sumcubes  42959  hbtlem5  43742  brfvtrcld  44334  corcltrcl  44352  fourierdlem50  46757  fourierdlem102  46809  fourierdlem114  46821  fmtnoinf  48172  fmtnofac2  48205