Theorem nnssnn0 12404

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

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  0cc0 11026  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-n0 12402

This theorem is referenced by:  nnnn0  12408  nnnn0d  12462  nthruz  16178  oddge22np1  16276  bitsfzolem  16361  lcmfval  16548  ramub1  16956  ramcl  16957  ply1divex  26098  pserdvlem2  26394  2sqreunnlem1  27416  2sqreunnlem2  27422  fsum2dsub  34764  breprexplemc  34789  breprexpnat  34791  knoppndvlem18  36729  sumcubes  42568  hbtlem5  43370  brfvtrcld  43962  corcltrcl  43980  fourierdlem50  46400  fourierdlem102  46452  fourierdlem114  46464  fmtnoinf  47782  fmtnofac2  47815