Theorem nnssnn0 11754

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 4075	. 2 ⊢ ℕ ⊆ (ℕ ∪ {0})
2		df-n0 11752	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
3	1, 2	sseqtr4i 3931	1 ⊢ ℕ ⊆ ℕ0

Syntax hints:   ∪ cun 3863   ⊆ wss 3865  {csn 4478  0cc0 10390  ℕcn 11492  ℕ₀cn0 11751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-in 3872  df-ss 3880  df-n0 11752

This theorem is referenced by:  nnnn0  11758  nnnn0d  11809  nthruz  15443  oddge22np1  15535  bitsfzolem  15620  lcmfval  15798  ramub1  16197  ramcl  16198  ply1divex  24417  pserdvlem2  24703  2sqreunnlem1  25711  2sqreunnlem2  25717  fsum2dsub  31491  breprexplemc  31516  breprexpnat  31518  knoppndvlem18  33479  hbtlem5  39234  brfvtrcld  39572  corcltrcl  39590  fourierdlem50  42005  fourierdlem102  42057  fourierdlem114  42069  fmtnoinf  43202  fmtnofac2  43235