Theorem nnnn0d 9188

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 8878  ℕ₀cn0 9135

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-n0 9136

This theorem is referenced by:  nn0ge2m1nn0  9196  nnzd  9333  eluzge2nn0  9528  modsumfzodifsn  10352  addmodlteq  10354  expnnval  10479  expgt1  10514  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  expnbnd  10599  facwordi  10674  faclbnd  10675  facavg  10680  bcm1k  10694  bcval5  10697  1elfz0hash  10741  resqrexlemnm  10982  resqrexlemcvg  10983  summodc  11346  zsumdc  11347  bcxmas  11452  geo2sum  11477  geo2lim  11479  geoisum1  11482  geoisum1c  11483  cvgratnnlembern  11486  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  mertenslemi1  11498  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  eftabs  11619  efcllemp  11621  eftlub  11653  eirraplem  11739  dvdsfac  11820  divalglemnqt  11879  divalglemeunn  11880  gcdval  11914  gcdcl  11921  dvdsgcdidd  11949  mulgcd  11971  rplpwr  11982  rppwr  11983  lcmcl  12026  lcmgcdnn  12036  nprmdvds1  12094  isprm5lem  12095  rpexp  12107  pw2dvdslemn  12119  sqpweven  12129  2sqpwodd  12130  nn0sqrtelqelz  12160  phiprmpw  12176  crth  12178  eulerthlema  12184  eulerthlemth  12186  eulerth  12187  fermltl  12188  odzcllem  12196  odzdvds  12199  odzphi  12200  modprm0  12208  prm23lt5  12217  pythagtriplem6  12224  pythagtriplem7  12225  pcprmpw2  12286  dvdsprmpweqle  12290  pcprod  12298  pcfac  12302  pcbc  12303  expnprm  12305  pockthlem  12308  pockthg  12309  prmunb  12314  mul4sqlem  12345  logbgcd1irraplemexp  13680  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsvalmod  13714  lgsmod  13721  lgsdirprm  13729  lgsne0  13733  2sqlem3  13747  cvgcmp2nlemabs  14064  trilpolemlt1  14073  redcwlpolemeq1  14086  nconstwlpolem0  14094