Theorem nnssnn0 11901

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

Syntax hints:   ∪ cun 3934   ⊆ wss 3936  {csn 4567  0cc0 10537  ℕcn 11638  ℕ₀cn0 11898

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-n0 11899

This theorem is referenced by:  nnnn0  11905  nnnn0d  11956  nthruz  15606  oddge22np1  15698  bitsfzolem  15783  lcmfval  15965  ramub1  16364  ramcl  16365  ply1divex  24730  pserdvlem2  25016  2sqreunnlem1  26025  2sqreunnlem2  26031  fsum2dsub  31878  breprexplemc  31903  breprexpnat  31905  knoppndvlem18  33868  hbtlem5  39748  brfvtrcld  40086  corcltrcl  40104  fourierdlem50  42461  fourierdlem102  42513  fourierdlem114  42525  fmtnoinf  43718  fmtnofac2  43751