Theorem fveq1i 6818

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fveq1i	⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fveq1 6816	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1541  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484

This theorem is referenced by:  fveq12i  6823  fvun2  6909  fvopab3ig  6920  fvsnun1  7111  fvpr1g  7119  fvpr2g  7120  fvtp1  7124  fvtp2  7125  fvtp3  7126  fvtp1g  7127  fvtp2g  7128  fvtp3g  7129  fpropnf1  7196  fveqf1o  7231  ov  7485  ovigg  7486  ovg  7506  fvresex  7887  curry1  8029  curry2  8032  fsplitfpar  8043  suppsnop  8103  frrlem12  8222  fprlem1  8225  tfr2a  8309  rdgsucmptf  8342  rdgsucmptnf  8343  frsucmpt  8352  frsucmptn  8353  seqomlem1  8364  seqomlem3  8366  seqomlem4  8367  seqom0g  8370  seqomsuc  8371  unblem2  9172  inf3lemb  9510  inf3lemc  9511  ttrclselem1  9610  ttrclselem2  9611  trcl  9613  frrlem15  9645  r10  9656  r1sucg  9657  r1limg  9659  infxpenc2  9908  aleph0  9952  alephlim  9953  alephsuc  9954  alephfplem1  9990  alephfplem2  9991  ackbij2lem3  10126  cfsmolem  10156  infpssrlem1  10189  infpssrlem2  10190  fin23lem34  10232  fin23lem35  10233  isf32lem6  10244  isf32lem7  10245  isf32lem8  10246  isf34lem5  10264  hsmexlem7  10309  axdclem2  10406  canthp1lem2  10539  wunex2  10624  wuncval2  10633  addpiord  10770  mulpiord  10771  addpqnq  10824  mulpqnq  10827  fseq1p1m1  13493  om2uz0i  13849  om2uzrdg  13858  uzrdg0i  13861  uzrdgsuci  13862  hashkf  14234  hashgval  14235  hashinf  14237  ccat1st1st  14531  revs1  14667  cats1fv  14761  shftidt  14984  cbvsum  15597  cbvsumv  15598  fsumss  15627  isumclim3  15661  isumsup2  15748  cbvprod  15815  cbvprodv  15816  fprodss  15850  iprodclim3  15902  fprodefsum  15997  ruclem4  16138  ruclem6  16139  ruclem7  16140  sadc0  16360  sadcp1  16361  sadcaddlem  16363  sadaddlem  16372  smup0  16385  smupp1  16386  algr0  16478  algrp1  16480  ndxarg  17102  strfv2d  17107  funcoppc  17777  fthepi  17832  homadm  17942  homacd  17943  prdsidlem  18672  prdsinvlem  18957  cayleylem2  19320  symggen  19377  pmtr3ncomlem1  19380  gsumval3  19814  gsumzaddlem  19828  gsumzmhm  19844  pgpfaclem1  19990  ringidval  20096  rhmsubclem2  20596  lidlval  21142  rspval  21143  lidlnegcl  21154  lpival  21256  znf1o  21483  ply1ascl0  22162  ply1ascl1  22163  eqcoe1ply1eq  22209  evls1val  22230  evl1val  22239  mat1dimmul  22386  mdetralt  22518  mdetunilem7  22528  decpmatid  22680  pmatcollpwscmatlem1  22699  cpmidpmat  22783  chcoeffeq  22796  restcls  23091  restntr  23092  upxp  23533  cnmetdval  24680  remetdval  24699  qdensere2  24707  pcoptcl  24943  pcopt  24944  pcopt2  24945  pcorevlem  24948  isncvsngp  25071  cnncvsabsnegdemo  25087  ovolfsval  25393  ovollb2lem  25411  ovolunlem1a  25419  ovoliunlem1  25425  ovoliun2  25429  ovolscalem1  25436  ovolicc2lem4  25443  mblvol  25453  ioombl1lem4  25484  uniioovol  25502  uniioombllem3  25508  0pval  25594  limccnp  25814  limccnp2  25815  dvcnvrelem2  25945  itgsubstlem  25977  ply1remlem  26092  plyrem  26235  qaa  26253  abelth  26373  efif1olem4  26476  eflog  26507  logef  26512  logeftb  26514  dvrelog  26568  dvlog  26582  cxpcn3  26680  efrlim  26901  efrlimOLD  26902  eflgam  26977  wilthlem3  27002  basellem8  27020  lgsqrlem1  27279  noetasuplem4  27670  noetainflem4  27674  precsexlem1  28140  precsexlem2  28141  precsexlem3  28142  precsexlem4  28143  precsexlem5  28144  tgcgr4  28504  krippenlem  28663  colperpexlem1  28703  opphllem3  28722  lmiisolem  28769  axlowdimlem8  28922  axlowdimlem9  28923  axlowdimlem11  28925  axlowdimlem12  28926  axlowdimlem17  28931  ushgredgedg  29202  ushgredgedgloop  29204  subgruhgredgd  29257  vtxdlfgrval  29459  vtxd0nedgb  29462  vtxdushgrfvedg  29464  vtxdginducedm1lem3  29515  finsumvtxdg2size  29524  vtxdgoddnumeven  29527  isrgr  29533  fusgrregdegfi  29543  wlk1walk  29612  wlkres  29642  wlkp1lem5  29649  wlkp1lem6  29650  wlkp1lem7  29651  wlkp1lem8  29652  clwlkcompbp  29755  crctcshwlkn0lem4  29786  crctcshwlkn0lem5  29787  crctcshwlkn0lem6  29788  2wlkdlem3  29900  2wlkdlem8  29906  2wlkond  29910  umgr2adedgwlk  29918  1wlkdlem4  30112  1pthond  30116  wlk2v2elem2  30128  3wlkdlem3  30133  3wlkdlem8  30139  3cycld  30150  3cyclpd  30151  eucrctshift  30215  frgrncvvdeq  30281  frgrwopreglem2  30285  ex-fpar  30434  avril1  30435  vafval  30575  smfval  30577  0vfval  30578  nmcvfval  30579  vsfval  30605  hhssabloilem  31233  pjoc2i  31410  pjcji  31656  ho0val  31722  hoival  31727  adjbdlnb  32056  nmopcoadji  32073  opsqrlem2  32113  opsqrlem5  32116  hmopidmchi  32123  hmopidmpji  32124  pjinvari  32163  pjadj2coi  32176  pj3lem1  32178  funcnvmpt  32641  pmtrprfv2  33049  cycpmco2lem7  33093  evl1fpws  33519  rgmoddimOLD  33615  rtelextdg2lem  33731  constr0  33742  constrsuc  33743  constrlim  33744  2sqr3minply  33785  cos9thpiminplylem6  33792  madjusmdetlem1  33832  cnre2csqlem  33915  zzsnm  33964  rrhcn  34002  qqhre  34025  oms0  34302  omsmon  34303  omssubaddlem  34304  omssubadd  34305  eulerpart  34387  fib0  34404  fib1  34405  fibp1  34406  coinflippv  34489  gsumnunsn  34546  2cycld  35174  derangenlem  35207  kur14lem2  35243  kur14lem3  35244  kur14lem5  35246  kur14lem6  35247  txsconnlem  35276  cvmliftlem4  35324  cvmliftlem5  35325  satf0sucom  35409  satf0suc  35412  satf0op  35413  fmla  35417  satffunlem2lem2  35442  satfv0fvfmla0  35449  sate0  35451  funpartfv  35979  fullfunfv  35981  sumeq2si  36236  prodeq2si  36238  cbvprodvw2  36281  neibastop2lem  36394  dffinxpf  37419  ftc1cnnc  37732  heiborlem4  37854  heiborlem6  37856  cdlemk13  40891  cdlemk14  40893  cdlemk15  40894  cdlemk21N  40912  cdlemk20  40913  cdlemk56w  41012  lcfrlem1  41581  hdmapfval  41866  deg1gprod  42173  evlsevl  42604  selvvvval  42618  rabdiophlem2  42835  dnnumch1  43077  aomclem6  43092  mncn0  43172  aaitgo  43195  rngunsnply  43202  cytpval  43235  dssmapntrcls  44161  binomcxplemdvsum  44388  binomcxplemnotnn0  44389  binomcxp  44390  fvcod  45264  fvmpt2df  45309  fsumsermpt  45619  fmul01  45620  fmuldfeq  45623  fmul01lt1lem1  45624  fmul01lt1lem2  45625  lptioo2cn  45683  lptioo1cn  45684  limclner  45689  dvsinax  45951  fperdvper  45957  dvnmul  45981  dvnprodlem1  45984  dvnprodlem2  45985  dvnprodlem3  45986  itgsin0pilem1  45988  stoweidlem3  46041  stoweidlem17  46055  stoweidlem47  46085  fourierdlem42  46187  fourierdlem62  46206  fourierdlem80  46224  fourierdlem90  46234  fourierdlem92  46236  fourierdlem93  46237  fourierdlem103  46247  fourierdlem104  46248  fouriercnp  46264  sge0isum  46465  sge0seq  46484  ovnsubadd  46610  vonn0ioo  46725  vonn0icc  46726  smflimsup  46866  cjnpoly  46920  sinnpoly  46922  fcores  47098  fundcmpsurinjimaid  47442  isgrim  47913  gricushgr  47948  gpgprismgr4cycllem3  48128  gpgprismgr4cycllem6  48131  gpgprismgr4cycllem7  48132  gpgprismgr4cycllem10  48135  rhmsubcALTVlem2  48313  ply1mulgsum  48422  lineval  48426  lincvalpr  48450  lindslinindimp2lem4  48493  zlmodzxzldeplem3  48534  zlmodzxzldeplem4  48535  itcoval0mpt  48698  ackvalsuc1mpt  48710  ackval0  48712  ackval40  48725  ackval41a  48726  ackval42  48728  ackval50  48730  ehl2eudisval0  48757  2sphere0  48782  line2  48784  line2x  48786  line2y  48787  itscnhlinecirc02p  48817  oppcup  49239  natoppf  49261