Theorem nnnn0d 9455

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9143  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-n0 9403

This theorem is referenced by:  nn0ge2m1nn0  9463  nnzd  9601  eluzge2nn0  9804  modsumfzodifsn  10659  addmodlteq  10661  expnnval  10805  expgt1  10840  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  expnbnd  10926  facwordi  11003  faclbnd  11004  facavg  11009  bcm1k  11023  bcval5  11026  1elfz0hash  11071  pfxfvlsw  11280  wrdeqs1cat  11305  resqrexlemnm  11596  resqrexlemcvg  11597  summodc  11962  zsumdc  11963  bcxmas  12068  geo2sum  12093  geo2lim  12095  geoisum1  12098  geoisum1c  12099  cvgratnnlembern  12102  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  mertenslemi1  12114  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  eftabs  12235  efcllemp  12237  eftlub  12269  eirraplem  12356  dvdsfac  12439  divalglemnqt  12499  divalglemeunn  12500  bitsfzo  12534  bitsfi  12536  gcdval  12548  gcdcl  12555  dvdsgcdidd  12583  mulgcd  12605  rplpwr  12616  rppwr  12617  lcmcl  12662  lcmgcdnn  12672  nprmdvds1  12730  isprm5lem  12731  rpexp  12743  pw2dvdslemn  12755  sqpweven  12765  2sqpwodd  12766  nn0sqrtelqelz  12796  phiprmpw  12812  crth  12814  eulerthlema  12820  eulerthlemth  12822  eulerth  12823  fermltl  12824  odzcllem  12833  odzdvds  12836  odzphi  12837  modprm0  12845  prm23lt5  12854  pythagtriplem6  12861  pythagtriplem7  12862  pcprmpw2  12924  dvdsprmpweqle  12928  pcprod  12937  pcfac  12941  pcbc  12942  expnprm  12944  pockthlem  12947  pockthg  12948  prmunb  12953  mul4sqlem  12984  4sqlem11  12992  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  2expltfac  13030  znf1o  14684  dvply1  15508  logbgcd1irraplemexp  15711  wilthlem1  15723  mpodvdsmulf1o  15733  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsvalmod  15767  lgsmod  15774  lgsdirprm  15782  lgsne0  15786  gausslemma2dlem0b  15798  gausslemma2dlem0c  15799  gausslemma2dlem1  15809  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem2  15826  lgsquadlem3  15827  m1lgs  15833  2lgslem1a  15836  2sqlem3  15865  isclwwlkn  16283  clwwlknccat  16293  clwwlknon  16299  depindlem1  16376  cvgcmp2nlemabs  16687  trilpolemlt1  16696  redcwlpolemeq1  16710  nconstwlpolem0  16719