Theorem nnnn0d 9223

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8913  ℕ₀cn0 9170

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-n0 9171

This theorem is referenced by:  nn0ge2m1nn0  9231  nnzd  9368  eluzge2nn0  9563  modsumfzodifsn  10389  addmodlteq  10391  expnnval  10516  expgt1  10551  expaddzaplem  10556  expaddzap  10557  expmulzap  10559  expnbnd  10636  facwordi  10711  faclbnd  10712  facavg  10717  bcm1k  10731  bcval5  10734  1elfz0hash  10777  resqrexlemnm  11018  resqrexlemcvg  11019  summodc  11382  zsumdc  11383  bcxmas  11488  geo2sum  11513  geo2lim  11515  geoisum1  11518  geoisum1c  11519  cvgratnnlembern  11522  cvgratnnlemsumlt  11527  cvgratnnlemfm  11528  mertenslemi1  11534  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  fprodseq  11582  eftabs  11655  efcllemp  11657  eftlub  11689  eirraplem  11775  dvdsfac  11856  divalglemnqt  11915  divalglemeunn  11916  gcdval  11950  gcdcl  11957  dvdsgcdidd  11985  mulgcd  12007  rplpwr  12018  rppwr  12019  lcmcl  12062  lcmgcdnn  12072  nprmdvds1  12130  isprm5lem  12131  rpexp  12143  pw2dvdslemn  12155  sqpweven  12165  2sqpwodd  12166  nn0sqrtelqelz  12196  phiprmpw  12212  crth  12214  eulerthlema  12220  eulerthlemth  12222  eulerth  12223  fermltl  12224  odzcllem  12232  odzdvds  12235  odzphi  12236  modprm0  12244  prm23lt5  12253  pythagtriplem6  12260  pythagtriplem7  12261  pcprmpw2  12322  dvdsprmpweqle  12326  pcprod  12334  pcfac  12338  pcbc  12339  expnprm  12341  pockthlem  12344  pockthg  12345  prmunb  12350  mul4sqlem  12381  logbgcd1irraplemexp  14168  lgslem1  14183  lgsval  14187  lgsfvalg  14188  lgsval2lem  14193  lgsvalmod  14202  lgsmod  14209  lgsdirprm  14217  lgsne0  14221  2sqlem3  14235  cvgcmp2nlemabs  14551  trilpolemlt1  14560  redcwlpolemeq1  14573  nconstwlpolem0  14581