Theorem nnssnn0 12093

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

Syntax hints:   ∪ cun 3864   ⊆ wss 3866  {csn 4541  0cc0 10729  ℕcn 11830  ℕ₀cn0 12090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-in 3873  df-ss 3883  df-n0 12091

This theorem is referenced by:  nnnn0  12097  nnnn0d  12150  nthruz  15814  oddge22np1  15910  bitsfzolem  15993  lcmfval  16178  ramub1  16581  ramcl  16582  ply1divex  25034  pserdvlem2  25320  2sqreunnlem1  26330  2sqreunnlem2  26336  fsum2dsub  32299  breprexplemc  32324  breprexpnat  32326  knoppndvlem18  34446  hbtlem5  40656  brfvtrcld  41006  corcltrcl  41024  fourierdlem50  43372  fourierdlem102  43424  fourierdlem114  43436  fmtnoinf  44661  fmtnofac2  44694