Theorem nnssnn0 11903

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

Syntax hints:   ∪ cun 3936   ⊆ wss 3938  {csn 4569  0cc0 10539  ℕcn 11640  ℕ₀cn0 11900

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-n0 11901

This theorem is referenced by:  nnnn0  11907  nnnn0d  11958  nthruz  15608  oddge22np1  15700  bitsfzolem  15785  lcmfval  15967  ramub1  16366  ramcl  16367  ply1divex  24732  pserdvlem2  25018  2sqreunnlem1  26027  2sqreunnlem2  26033  fsum2dsub  31880  breprexplemc  31905  breprexpnat  31907  knoppndvlem18  33870  hbtlem5  39735  brfvtrcld  40073  corcltrcl  40091  fourierdlem50  42448  fourierdlem102  42500  fourierdlem114  42512  fmtnoinf  43705  fmtnofac2  43738