Theorem nnnn0d 9555

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 9501	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3238	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2205  ℕcn 9239  ℕ₀cn0 9498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-n0 9499

This theorem is referenced by:  nn0ge2m1nn0  9563  nnzd  9702  eluzge2nn0  9905  modsumfzodifsn  10762  addmodlteq  10764  expnnval  10908  expgt1  10943  expaddzaplem  10948  expaddzap  10949  expmulzap  10951  expnbnd  11029  facwordi  11106  faclbnd  11107  facavg  11112  bcm1k  11126  bcval5  11129  bcm1n  11135  1elfz0hash  11175  pfxfvlsw  11391  wrdeqs1cat  11416  resqrexlemnm  11707  resqrexlemcvg  11708  summodc  12073  zsumdc  12074  bcxmas  12179  geo2sum  12204  geo2lim  12206  geoisum1  12209  geoisum1c  12210  cvgratnnlembern  12213  cvgratnnlemsumlt  12218  cvgratnnlemfm  12219  mertenslemi1  12225  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  eftabs  12346  efcllemp  12348  eftlub  12380  eirraplem  12467  dvdsfac  12550  divalglemnqt  12610  divalglemeunn  12611  bitsfzo  12645  bitsfi  12647  gcdval  12659  gcdcl  12666  dvdsgcdidd  12694  mulgcd  12716  rplpwr  12727  rppwr  12728  lcmcl  12773  lcmgcdnn  12783  nprmdvds1  12841  isprm5lem  12842  rpexp  12854  pw2dvdslemn  12866  sqpweven  12876  2sqpwodd  12877  nn0sqrtelqelz  12907  phiprmpw  12923  crth  12925  eulerthlema  12931  eulerthlemth  12933  eulerth  12934  fermltl  12935  odzcllem  12944  odzdvds  12947  odzphi  12948  modprm0  12956  prm23lt5  12965  pythagtriplem6  12972  pythagtriplem7  12973  pcprmpw2  13035  dvdsprmpweqle  13039  pcprod  13048  pcfac  13052  pcbc  13053  expnprm  13055  pockthlem  13058  pockthg  13059  prmunb  13064  mul4sqlem  13095  4sqlem11  13103  4sqlem13m  13105  4sqlem14  13106  4sqlem17  13109  4sqlem18  13110  2expltfac  13141  znf1o  14816  dvply1  15647  logbgcd1irraplemexp  15850  pellexlem2  15863  wilthlem1  15865  mpodvdsmulf1o  15875  mersenne  15882  perfect1  15883  perfectlem1  15884  perfectlem2  15885  perfect  15886  lgslem1  15890  lgsval  15894  lgsfvalg  15895  lgsval2lem  15900  lgsvalmod  15909  lgsmod  15916  lgsdirprm  15924  lgsne0  15928  gausslemma2dlem0b  15940  gausslemma2dlem0c  15941  gausslemma2dlem1  15951  gausslemma2dlem7  15958  gausslemma2d  15959  lgseisenlem1  15960  lgseisenlem2  15961  lgseisenlem3  15962  lgseisenlem4  15963  lgseisen  15964  lgsquadlem2  15968  lgsquadlem3  15969  m1lgs  15975  2lgslem1a  15978  2sqlem3  16007  isclwwlkn  16425  clwwlknccat  16435  clwwlknon  16441  depindlem1  16518  cvgcmp2nlemabs  16833  trilpolemlt1  16842  redcwlpolemeq1  16856  nconstwlpolem0  16866