Theorem nnssnn0 12518

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

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906  {csn 4591  0cc0 11111  ℕcn 12244  ℕ₀cn0 12515

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-n0 12516

This theorem is used by:  nnnn0  12522  nnnn0d  12576  nthruz  16327  oddge22np1  16425  bitsfzolem  16510  lcmfval  16697  ramub1  17106  ramcl  17107  ply1divex  26325  pserdvlem2  26622  2sqreunnlem1  27644  2sqreunnlem2  27650  fsum2dsub  35035  breprexplemc  35060  breprexpnat  35062  knoppndvlem18  37151  sumcubes  43107  hbtlem5  43888  brfvtrcld  44480  corcltrcl  44498  fourierdlem50  46903  fourierdlem102  46955  fourierdlem114  46967  fmtnoinf  48321  fmtnofac2  48354