Theorem nnssnn0 12405

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4579  0cc0 11028  ℕcn 12146  ℕ₀cn0 12402

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 3440  df-un 3910  df-ss 3922  df-n0 12403

This theorem is referenced by:  nnnn0  12409  nnnn0d  12463  nthruz  16180  oddge22np1  16278  bitsfzolem  16363  lcmfval  16550  ramub1  16958  ramcl  16959  ply1divex  26058  pserdvlem2  26354  2sqreunnlem1  27376  2sqreunnlem2  27382  fsum2dsub  34577  breprexplemc  34602  breprexpnat  34604  knoppndvlem18  36505  sumcubes  42289  hbtlem5  43104  brfvtrcld  43697  corcltrcl  43715  fourierdlem50  46141  fourierdlem102  46193  fourierdlem114  46205  fmtnoinf  47524  fmtnofac2  47557