Theorem nnssnn0 12445

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

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  0cc0 11068  ℕcn 12186  ℕ₀cn0 12442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-n0 12443

This theorem is referenced by:  nnnn0  12449  nnnn0d  12503  nthruz  16221  oddge22np1  16319  bitsfzolem  16404  lcmfval  16591  ramub1  16999  ramcl  17000  ply1divex  26042  pserdvlem2  26338  2sqreunnlem1  27360  2sqreunnlem2  27366  fsum2dsub  34598  breprexplemc  34623  breprexpnat  34625  knoppndvlem18  36517  sumcubes  42301  hbtlem5  43117  brfvtrcld  43710  corcltrcl  43728  fourierdlem50  46154  fourierdlem102  46206  fourierdlem114  46218  fmtnoinf  47537  fmtnofac2  47570