Theorem nnnn0d 9499

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 9447	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3226	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9185  ℕ₀cn0 9444

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-n0 9445

This theorem is referenced by:  nn0ge2m1nn0  9507  nnzd  9645  eluzge2nn0  9848  modsumfzodifsn  10704  addmodlteq  10706  expnnval  10850  expgt1  10885  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  expnbnd  10971  facwordi  11048  faclbnd  11049  facavg  11054  bcm1k  11068  bcval5  11071  1elfz0hash  11116  pfxfvlsw  11325  wrdeqs1cat  11350  resqrexlemnm  11641  resqrexlemcvg  11642  summodc  12007  zsumdc  12008  bcxmas  12113  geo2sum  12138  geo2lim  12140  geoisum1  12143  geoisum1c  12144  cvgratnnlembern  12147  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  mertenslemi1  12159  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  eftabs  12280  efcllemp  12282  eftlub  12314  eirraplem  12401  dvdsfac  12484  divalglemnqt  12544  divalglemeunn  12545  bitsfzo  12579  bitsfi  12581  gcdval  12593  gcdcl  12600  dvdsgcdidd  12628  mulgcd  12650  rplpwr  12661  rppwr  12662  lcmcl  12707  lcmgcdnn  12717  nprmdvds1  12775  isprm5lem  12776  rpexp  12788  pw2dvdslemn  12800  sqpweven  12810  2sqpwodd  12811  nn0sqrtelqelz  12841  phiprmpw  12857  crth  12859  eulerthlema  12865  eulerthlemth  12867  eulerth  12868  fermltl  12869  odzcllem  12878  odzdvds  12881  odzphi  12882  modprm0  12890  prm23lt5  12899  pythagtriplem6  12906  pythagtriplem7  12907  pcprmpw2  12969  dvdsprmpweqle  12973  pcprod  12982  pcfac  12986  pcbc  12987  expnprm  12989  pockthlem  12992  pockthg  12993  prmunb  12998  mul4sqlem  13029  4sqlem11  13037  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  2expltfac  13075  znf1o  14730  dvply1  15559  logbgcd1irraplemexp  15762  pellexlem2  15775  wilthlem1  15777  mpodvdsmulf1o  15787  mersenne  15794  perfect1  15795  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgslem1  15802  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsvalmod  15821  lgsmod  15828  lgsdirprm  15836  lgsne0  15840  gausslemma2dlem0b  15852  gausslemma2dlem0c  15853  gausslemma2dlem1  15863  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlem2  15880  lgsquadlem3  15881  m1lgs  15887  2lgslem1a  15890  2sqlem3  15919  isclwwlkn  16337  clwwlknccat  16347  clwwlknon  16353  depindlem1  16430  cvgcmp2nlemabs  16747  trilpolemlt1  16756  redcwlpolemeq1  16770  nconstwlpolem0  16779