Theorem nnnn0 9008

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 9004	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3098	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 1481  ℕcn 8744  ℕ₀cn0 9001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-n0 9002

This theorem is referenced by:  nnnn0i  9009  elnnnn0b  9045  elnnnn0c  9046  elnn0z  9091  elz2  9146  nn0ind-raph  9192  zindd  9193  fzo1fzo0n0  9991  ubmelfzo  10008  elfzom1elp1fzo  10010  fzo0sn0fzo1  10029  modqmulnn  10146  expnegap0  10332  expcllem  10335  expcl2lemap  10336  expap0  10354  expeq0  10355  mulexpzap  10364  expnlbnd  10447  apexp1  10496  facdiv  10516  faclbnd  10519  faclbnd3  10521  faclbnd6  10522  resqrexlemlo  10817  absexpzap  10884  nnf1o  11177  summodclem2a  11182  fsum3  11188  arisum  11299  expcnvap0  11303  expcnv  11305  geo2sum  11315  geo2lim  11317  geoisum1c  11321  0.999...  11322  mertenslem2  11337  fprodseq  11384  ef0lem  11403  ege2le3  11414  efaddlem  11417  efexp  11425  nn0enne  11635  nnehalf  11637  nno  11639  nn0o  11640  divalg2  11659  ndvdssub  11663  gcddiv  11743  gcdmultiple  11744  gcdmultiplez  11745  rpmulgcd  11750  rplpwr  11751  dvdssqlem  11754  eucalgf  11772  1nprm  11831  isprm6  11861  prmdvdsexp  11862  pw2dvds  11880  oddpwdc  11888  phicl2  11926  phibndlem  11928  phiprmpw  11934  crth  11936  hashgcdlem  11939  ennnfonelemjn  11951  dvexp  12883  logbgcd1irr  13092