Theorem nnnn0 9575

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 9571	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3244	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9307  ℕ₀cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-n0 9569

This theorem is used by:  nnnn0i  9576  elnnnn0b  9612  elnnnn0c  9613  elnn0z  9662  elz2  9721  nn0ind-raph  9768  zindd  9769  fzo1fzo0n0  10606  ubmelfzo  10629  elfzom1elp1fzo  10631  fzo0sn0fzo1  10650  modqmulnn  10794  expnegap0  10999  expcllem  11002  expcl2lemap  11003  expap0  11021  expeq0  11022  mulexpzap  11031  expnlbnd  11117  apexp1  11172  facdiv  11192  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  pfxn0  11476  resqrexlemlo  11795  absexpzap  11863  nnf1o  12162  summodclem2a  12167  fsum3  12173  arisum  12284  expcnvap0  12288  expcnv  12290  geo2sum  12300  geo2lim  12302  geoisum1c  12306  0.999...  12307  mertenslem2  12322  fprodseq  12369  fprodfac  12401  ef0lem  12446  ege2le3  12457  efaddlem  12460  efexp  12468  dvdsmodexp  12581  nn0enne  12688  nnehalf  12690  nno  12692  nn0o  12693  divalg2  12712  ndvdssub  12716  gcddiv  12815  gcdmultiple  12816  gcdmultiplez  12817  rpmulgcd  12822  rplpwr  12823  dvdssqlem  12826  eucalgf  12852  1nprm  12911  isprm6  12945  prmdvdsexp  12946  pwbdvdslemn  12963  phicl2  13015  phibndlem  13017  phiprmpw  13023  crth  13025  hashgcdlem  13039  phisum  13042  pythagtriplem10  13071  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pclemub  13089  pcexp  13111  pcid  13126  pcprod  13148  pcbc  13153  prmpwdvds  13157  infpnlem1  13161  infpnlem2  13162  prmunb  13164  1arith  13169  ennnfonelemjn  13345  ghmmulg  14112  znf1o  15070  znfi  15074  znhash  15075  znidom  15076  znidomb  15077  znrrg  15079  dvexp  15903  plycolemc  15950  logbgcd1irr  16169  birthdaylem2  16192  birthdaylem3  16193  pellexlem1  16195  1sgm2ppw  16255  chtublem  16261  pcbcctr  16269  bclbnd  16273  bposlem1  16277  lgsval4a  16312  gausslemma2dlem0c  16341  gausslemma2dlem0d  16342  gausslemma2dlem6  16357  2lgslem1a1  16376  2lgslem1c  16380  2lgslem3a1  16387  2lgslem3b1  16388  2lgslem3c1  16389  2lgslem3d1  16390  isclwwlknx  16828