Theorem nnssnn0 12649

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

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  0cc0 11239  ℕcn 12375  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-n0 12647

This theorem is used by:  nnnn0  12653  nnnn0d  12707  nthruz  16465  oddge22np1  16563  bitsfzolem  16648  lcmfval  16840  ramub1  17250  ramcl  17251  ply1divex  26510  pserdvlem2  26812  2sqreunnlem1  27833  2sqreunnlem2  27839  fsum2dsub  35347  breprexplemc  35372  breprexpnat  35374  knoppndvlem18  37610  sumcubes  43636  hbtlem5  44395  brfvtrcld  44982  corcltrcl  45000  hfstructcan  46298  fourierdlem50  47439  fourierdlem102  47491  fourierdlem114  47503  fmtnoinf  48894  fmtnofac2  48927