Theorem nnnn0d 9418

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9106  ℕ₀cn0 9365

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-n0 9366

This theorem is referenced by:  nn0ge2m1nn0  9426  nnzd  9564  eluzge2nn0  9760  modsumfzodifsn  10613  addmodlteq  10615  expnnval  10759  expgt1  10794  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  expnbnd  10880  facwordi  10957  faclbnd  10958  facavg  10963  bcm1k  10977  bcval5  10980  1elfz0hash  11023  pfxfvlsw  11222  wrdeqs1cat  11247  resqrexlemnm  11524  resqrexlemcvg  11525  summodc  11889  zsumdc  11890  bcxmas  11995  geo2sum  12020  geo2lim  12022  geoisum1  12025  geoisum1c  12026  cvgratnnlembern  12029  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  mertenslemi1  12041  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  eftabs  12162  efcllemp  12164  eftlub  12196  eirraplem  12283  dvdsfac  12366  divalglemnqt  12426  divalglemeunn  12427  bitsfzo  12461  bitsfi  12463  gcdval  12475  gcdcl  12482  dvdsgcdidd  12510  mulgcd  12532  rplpwr  12543  rppwr  12544  lcmcl  12589  lcmgcdnn  12599  nprmdvds1  12657  isprm5lem  12658  rpexp  12670  pw2dvdslemn  12682  sqpweven  12692  2sqpwodd  12693  nn0sqrtelqelz  12723  phiprmpw  12739  crth  12741  eulerthlema  12747  eulerthlemth  12749  eulerth  12750  fermltl  12751  odzcllem  12760  odzdvds  12763  odzphi  12764  modprm0  12772  prm23lt5  12781  pythagtriplem6  12788  pythagtriplem7  12789  pcprmpw2  12851  dvdsprmpweqle  12855  pcprod  12864  pcfac  12868  pcbc  12869  expnprm  12871  pockthlem  12874  pockthg  12875  prmunb  12880  mul4sqlem  12911  4sqlem11  12919  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  2expltfac  12957  znf1o  14609  dvply1  15433  logbgcd1irraplemexp  15636  wilthlem1  15648  mpodvdsmulf1o  15658  mersenne  15665  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgslem1  15673  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsvalmod  15692  lgsmod  15699  lgsdirprm  15707  lgsne0  15711  gausslemma2dlem0b  15723  gausslemma2dlem0c  15724  gausslemma2dlem1  15734  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem2  15751  lgsquadlem3  15752  m1lgs  15758  2lgslem1a  15761  2sqlem3  15790  cvgcmp2nlemabs  16359  trilpolemlt1  16368  redcwlpolemeq1  16381  nconstwlpolem0  16390