Theorem nnnn0d 8882

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnnn0d	|- ( ph -> A e. NN0 )

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 8832	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3045	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1448   NNcn 8578   NN0cn0 8829

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-n0 8830

This theorem is referenced by:  nn0ge2m1nn0  8890  nnzd  9024  eluzge2nn0  9215  modsumfzodifsn  10010  addmodlteq  10012  expnnval  10137  expgt1  10172  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  expnbnd  10256  facwordi  10327  faclbnd  10328  facavg  10333  bcm1k  10347  bcval5  10350  1elfz0hash  10393  resqrexlemnm  10630  resqrexlemcvg  10631  summodc  10991  zsumdc  10992  bcxmas  11097  geo2sum  11122  geo2lim  11124  geoisum1  11127  geoisum1c  11128  cvgratnnlembern  11131  cvgratnnlemsumlt  11136  cvgratnnlemfm  11137  mertenslemi1  11143  eftabs  11160  efcllemp  11162  eftlub  11194  eirraplem  11278  dvdsfac  11353  divalglemnqt  11412  divalglemeunn  11413  gcdval  11443  gcdcl  11450  mulgcd  11497  rplpwr  11508  rppwr  11509  lcmcl  11546  lcmgcdnn  11556  nprmdvds1  11613  rpexp  11624  pw2dvdslemn  11635  sqpweven  11645  2sqpwodd  11646  nn0sqrtelqelz  11676  phiprmpw  11690  crth  11692  cvgcmp2nlemabs  12811  trilpolemlt1  12818