Theorem fveq1i 6882

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 6880	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1540  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544

This theorem is referenced by:  fveq12i  6887  fvun2  6976  fvopab3ig  6987  fvsnun1  7179  fvpr1g  7187  fvpr2g  7188  fvtp1  7192  fvtp2  7193  fvtp3  7194  fvtp1g  7195  fvtp2g  7196  fvtp3g  7197  fpropnf1  7265  fveqf1o  7300  ov  7556  ovigg  7557  ovg  7577  fvresex  7963  curry1  8108  curry2  8111  fsplitfpar  8122  suppsnop  8182  frrlem12  8301  fprlem1  8304  wfrlem5OLD  8332  tfr2a  8414  rdgsucmptf  8447  rdgsucmptnf  8448  frsucmpt  8457  frsucmptn  8458  seqomlem1  8469  seqomlem3  8471  seqomlem4  8472  seqom0g  8475  seqomsuc  8476  unblem2  9306  inf3lemb  9644  inf3lemc  9645  ttrclselem1  9744  ttrclselem2  9745  trcl  9747  frrlem15  9776  r10  9787  r1sucg  9788  r1limg  9790  infxpenc2  10041  aleph0  10085  alephlim  10086  alephsuc  10087  alephfplem1  10123  alephfplem2  10124  ackbij2lem3  10259  cfsmolem  10289  infpssrlem1  10322  infpssrlem2  10323  fin23lem34  10365  fin23lem35  10366  isf32lem6  10377  isf32lem7  10378  isf32lem8  10379  isf34lem5  10397  hsmexlem7  10442  axdclem2  10539  canthp1lem2  10672  wunex2  10757  wuncval2  10766  addpiord  10903  mulpiord  10904  addpqnq  10957  mulpqnq  10960  fseq1p1m1  13620  om2uz0i  13970  om2uzrdg  13979  uzrdg0i  13982  uzrdgsuci  13983  hashkf  14355  hashgval  14356  hashinf  14358  ccat1st1st  14651  revs1  14788  cats1fv  14883  shftidt  15106  cbvsum  15716  cbvsumv  15717  fsumss  15746  isumclim3  15780  isumsup2  15867  cbvprod  15934  cbvprodv  15935  fprodss  15969  iprodclim3  16021  fprodefsum  16116  ruclem4  16257  ruclem6  16258  ruclem7  16259  sadc0  16478  sadcp1  16479  sadcaddlem  16481  sadaddlem  16490  smup0  16503  smupp1  16504  algr0  16596  algrp1  16598  ndxarg  17220  strfv2d  17225  funcoppc  17893  fthepi  17948  homadm  18058  homacd  18059  prdsidlem  18752  prdsinvlem  19037  cayleylem2  19399  symggen  19456  pmtr3ncomlem1  19459  gsumval3  19893  gsumzaddlem  19907  gsumzmhm  19923  pgpfaclem1  20069  ringidval  20148  rhmsubclem2  20651  lidlval  21176  rspval  21177  lidlnegcl  21188  lpival  21290  znf1o  21517  ply1ascl0  22195  ply1ascl1  22196  eqcoe1ply1eq  22242  evls1val  22263  evl1val  22272  mat1dimmul  22419  mdetralt  22551  mdetunilem7  22561  decpmatid  22713  pmatcollpwscmatlem1  22732  cpmidpmat  22816  chcoeffeq  22829  restcls  23124  restntr  23125  upxp  23566  cnmetdval  24714  remetdval  24733  qdensere2  24741  pcoptcl  24977  pcopt  24978  pcopt2  24979  pcorevlem  24982  isncvsngp  25106  cnncvsabsnegdemo  25122  ovolfsval  25428  ovollb2lem  25446  ovolunlem1a  25454  ovoliunlem1  25460  ovoliun2  25464  ovolscalem1  25471  ovolicc2lem4  25478  mblvol  25488  ioombl1lem4  25519  uniioovol  25537  uniioombllem3  25543  0pval  25629  limccnp  25849  limccnp2  25850  dvcnvrelem2  25980  itgsubstlem  26012  ply1remlem  26127  plyrem  26270  qaa  26288  abelth  26408  efif1olem4  26511  eflog  26542  logef  26547  logeftb  26549  dvrelog  26603  dvlog  26617  cxpcn3  26715  efrlim  26936  efrlimOLD  26937  eflgam  27012  wilthlem3  27037  basellem8  27055  lgsqrlem1  27314  noetasuplem4  27705  noetainflem4  27709  precsexlem1  28166  precsexlem2  28167  precsexlem3  28168  precsexlem4  28169  precsexlem5  28170  tgcgr4  28515  krippenlem  28674  colperpexlem1  28714  opphllem3  28733  lmiisolem  28780  axlowdimlem8  28933  axlowdimlem9  28934  axlowdimlem11  28936  axlowdimlem12  28937  axlowdimlem17  28942  ushgredgedg  29213  ushgredgedgloop  29215  subgruhgredgd  29268  vtxdlfgrval  29470  vtxd0nedgb  29473  vtxdushgrfvedg  29475  vtxdginducedm1lem3  29526  finsumvtxdg2size  29535  vtxdgoddnumeven  29538  isrgr  29544  fusgrregdegfi  29554  wlk1walk  29624  wlkres  29655  wlkp1lem5  29662  wlkp1lem6  29663  wlkp1lem7  29664  wlkp1lem8  29665  clwlkcompbp  29769  crctcshwlkn0lem4  29800  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  2wlkdlem3  29914  2wlkdlem8  29920  2wlkond  29924  umgr2adedgwlk  29932  1wlkdlem4  30126  1pthond  30130  wlk2v2elem2  30142  3wlkdlem3  30147  3wlkdlem8  30153  3cycld  30164  3cyclpd  30165  eucrctshift  30229  frgrncvvdeq  30295  frgrwopreglem2  30299  ex-fpar  30448  avril1  30449  vafval  30589  smfval  30591  0vfval  30592  nmcvfval  30593  vsfval  30619  hhssabloilem  31247  pjoc2i  31424  pjcji  31670  ho0val  31736  hoival  31741  adjbdlnb  32070  nmopcoadji  32087  opsqrlem2  32127  opsqrlem5  32130  hmopidmchi  32137  hmopidmpji  32138  pjinvari  32177  pjadj2coi  32190  pj3lem1  32192  funcnvmpt  32650  pmtrprfv2  33104  cycpmco2lem7  33148  evl1fpws  33582  rgmoddimOLD  33655  rtelextdg2lem  33765  constr0  33776  constrsuc  33777  constrlim  33778  2sqr3minply  33819  cos9thpiminplylem6  33826  madjusmdetlem1  33863  cnre2csqlem  33946  zzsnm  33995  rrhcn  34033  qqhre  34056  oms0  34334  omsmon  34335  omssubaddlem  34336  omssubadd  34337  eulerpart  34419  fib0  34436  fib1  34437  fibp1  34438  coinflippv  34521  gsumnunsn  34578  2cycld  35165  derangenlem  35198  kur14lem2  35234  kur14lem3  35235  kur14lem5  35237  kur14lem6  35238  txsconnlem  35267  cvmliftlem4  35315  cvmliftlem5  35316  satf0sucom  35400  satf0suc  35403  satf0op  35404  fmla  35408  satffunlem2lem2  35433  satfv0fvfmla0  35440  sate0  35442  funpartfv  35968  fullfunfv  35970  sumeq2si  36225  prodeq2si  36227  cbvprodvw2  36270  neibastop2lem  36383  dffinxpf  37408  ftc1cnnc  37721  heiborlem4  37843  heiborlem6  37845  cdlemk13  40876  cdlemk14  40878  cdlemk15  40879  cdlemk21N  40897  cdlemk20  40898  cdlemk56w  40997  lcfrlem1  41566  hdmapfval  41851  deg1gprod  42158  evlsevl  42569  selvvvval  42583  rabdiophlem2  42800  dnnumch1  43043  aomclem6  43058  mncn0  43138  aaitgo  43161  rngunsnply  43168  cytpval  43201  dssmapntrcls  44127  binomcxplemdvsum  44354  binomcxplemnotnn0  44355  binomcxp  44356  fvcod  45231  fvmpt2df  45276  fsumsermpt  45588  fmul01  45589  fmuldfeq  45592  fmul01lt1lem1  45593  fmul01lt1lem2  45594  lptioo2cn  45654  lptioo1cn  45655  limclner  45660  dvsinax  45922  fperdvper  45928  dvnmul  45952  dvnprodlem1  45955  dvnprodlem2  45956  dvnprodlem3  45957  itgsin0pilem1  45959  stoweidlem3  46012  stoweidlem17  46026  stoweidlem47  46056  fourierdlem42  46158  fourierdlem62  46177  fourierdlem80  46195  fourierdlem90  46205  fourierdlem92  46207  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  fouriercnp  46235  sge0isum  46436  sge0seq  46455  ovnsubadd  46581  vonn0ioo  46696  vonn0icc  46697  smflimsup  46837  fcores  47076  fundcmpsurinjimaid  47405  isgrim  47875  gricushgr  47910  gpgprismgr4cycllem3  48076  gpgprismgr4cycllem6  48079  gpgprismgr4cycllem7  48080  gpgprismgr4cycllem10  48083  rhmsubcALTVlem2  48237  ply1mulgsum  48346  lineval  48350  lincvalpr  48374  lindslinindimp2lem4  48417  zlmodzxzldeplem3  48458  zlmodzxzldeplem4  48459  itcoval0mpt  48626  ackvalsuc1mpt  48638  ackval0  48640  ackval40  48653  ackval41a  48654  ackval42  48656  ackval50  48658  ehl2eudisval0  48685  2sphere0  48710  line2  48712  line2x  48714  line2y  48715  itscnhlinecirc02p  48745  oppcup  49120