Theorem fveq1i 6841

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

Syntax hints:   = wceq 1540  ‘cfv 6499

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  fveq12i  6846  fvun2  6935  fvopab3ig  6946  fvsnun1  7138  fvpr1g  7146  fvpr2g  7147  fvtp1  7151  fvtp2  7152  fvtp3  7153  fvtp1g  7154  fvtp2g  7155  fvtp3g  7156  fpropnf1  7224  fveqf1o  7259  ov  7513  ovigg  7514  ovg  7534  fvresex  7918  curry1  8060  curry2  8063  fsplitfpar  8074  suppsnop  8134  frrlem12  8253  fprlem1  8256  tfr2a  8340  rdgsucmptf  8373  rdgsucmptnf  8374  frsucmpt  8383  frsucmptn  8384  seqomlem1  8395  seqomlem3  8397  seqomlem4  8398  seqom0g  8401  seqomsuc  8402  unblem2  9216  inf3lemb  9554  inf3lemc  9555  ttrclselem1  9654  ttrclselem2  9655  trcl  9657  frrlem15  9686  r10  9697  r1sucg  9698  r1limg  9700  infxpenc2  9951  aleph0  9995  alephlim  9996  alephsuc  9997  alephfplem1  10033  alephfplem2  10034  ackbij2lem3  10169  cfsmolem  10199  infpssrlem1  10232  infpssrlem2  10233  fin23lem34  10275  fin23lem35  10276  isf32lem6  10287  isf32lem7  10288  isf32lem8  10289  isf34lem5  10307  hsmexlem7  10352  axdclem2  10449  canthp1lem2  10582  wunex2  10667  wuncval2  10676  addpiord  10813  mulpiord  10814  addpqnq  10867  mulpqnq  10870  fseq1p1m1  13535  om2uz0i  13888  om2uzrdg  13897  uzrdg0i  13900  uzrdgsuci  13901  hashkf  14273  hashgval  14274  hashinf  14276  ccat1st1st  14569  revs1  14706  cats1fv  14801  shftidt  15024  cbvsum  15637  cbvsumv  15638  fsumss  15667  isumclim3  15701  isumsup2  15788  cbvprod  15855  cbvprodv  15856  fprodss  15890  iprodclim3  15942  fprodefsum  16037  ruclem4  16178  ruclem6  16179  ruclem7  16180  sadc0  16400  sadcp1  16401  sadcaddlem  16403  sadaddlem  16412  smup0  16425  smupp1  16426  algr0  16518  algrp1  16520  ndxarg  17142  strfv2d  17147  funcoppc  17813  fthepi  17868  homadm  17978  homacd  17979  prdsidlem  18672  prdsinvlem  18957  cayleylem2  19319  symggen  19376  pmtr3ncomlem1  19379  gsumval3  19813  gsumzaddlem  19827  gsumzmhm  19843  pgpfaclem1  19989  ringidval  20068  rhmsubclem2  20571  lidlval  21096  rspval  21097  lidlnegcl  21108  lpival  21210  znf1o  21437  ply1ascl0  22115  ply1ascl1  22116  eqcoe1ply1eq  22162  evls1val  22183  evl1val  22192  mat1dimmul  22339  mdetralt  22471  mdetunilem7  22481  decpmatid  22633  pmatcollpwscmatlem1  22652  cpmidpmat  22736  chcoeffeq  22749  restcls  23044  restntr  23045  upxp  23486  cnmetdval  24634  remetdval  24653  qdensere2  24661  pcoptcl  24897  pcopt  24898  pcopt2  24899  pcorevlem  24902  isncvsngp  25025  cnncvsabsnegdemo  25041  ovolfsval  25347  ovollb2lem  25365  ovolunlem1a  25373  ovoliunlem1  25379  ovoliun2  25383  ovolscalem1  25390  ovolicc2lem4  25397  mblvol  25407  ioombl1lem4  25438  uniioovol  25456  uniioombllem3  25462  0pval  25548  limccnp  25768  limccnp2  25769  dvcnvrelem2  25899  itgsubstlem  25931  ply1remlem  26046  plyrem  26189  qaa  26207  abelth  26327  efif1olem4  26430  eflog  26461  logef  26466  logeftb  26468  dvrelog  26522  dvlog  26536  cxpcn3  26634  efrlim  26855  efrlimOLD  26856  eflgam  26931  wilthlem3  26956  basellem8  26974  lgsqrlem1  27233  noetasuplem4  27624  noetainflem4  27628  precsexlem1  28085  precsexlem2  28086  precsexlem3  28087  precsexlem4  28088  precsexlem5  28089  tgcgr4  28434  krippenlem  28593  colperpexlem1  28633  opphllem3  28652  lmiisolem  28699  axlowdimlem8  28852  axlowdimlem9  28853  axlowdimlem11  28855  axlowdimlem12  28856  axlowdimlem17  28861  ushgredgedg  29132  ushgredgedgloop  29134  subgruhgredgd  29187  vtxdlfgrval  29389  vtxd0nedgb  29392  vtxdushgrfvedg  29394  vtxdginducedm1lem3  29445  finsumvtxdg2size  29454  vtxdgoddnumeven  29457  isrgr  29463  fusgrregdegfi  29473  wlk1walk  29542  wlkres  29572  wlkp1lem5  29579  wlkp1lem6  29580  wlkp1lem7  29581  wlkp1lem8  29582  clwlkcompbp  29685  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  crctcshwlkn0lem6  29718  2wlkdlem3  29830  2wlkdlem8  29836  2wlkond  29840  umgr2adedgwlk  29848  1wlkdlem4  30042  1pthond  30046  wlk2v2elem2  30058  3wlkdlem3  30063  3wlkdlem8  30069  3cycld  30080  3cyclpd  30081  eucrctshift  30145  frgrncvvdeq  30211  frgrwopreglem2  30215  ex-fpar  30364  avril1  30365  vafval  30505  smfval  30507  0vfval  30508  nmcvfval  30509  vsfval  30535  hhssabloilem  31163  pjoc2i  31340  pjcji  31586  ho0val  31652  hoival  31657  adjbdlnb  31986  nmopcoadji  32003  opsqrlem2  32043  opsqrlem5  32046  hmopidmchi  32053  hmopidmpji  32054  pjinvari  32093  pjadj2coi  32106  pj3lem1  32108  funcnvmpt  32564  pmtrprfv2  33018  cycpmco2lem7  33062  evl1fpws  33506  rgmoddimOLD  33579  rtelextdg2lem  33689  constr0  33700  constrsuc  33701  constrlim  33702  2sqr3minply  33743  cos9thpiminplylem6  33750  madjusmdetlem1  33790  cnre2csqlem  33873  zzsnm  33922  rrhcn  33960  qqhre  33983  oms0  34261  omsmon  34262  omssubaddlem  34263  omssubadd  34264  eulerpart  34346  fib0  34363  fib1  34364  fibp1  34365  coinflippv  34448  gsumnunsn  34505  2cycld  35098  derangenlem  35131  kur14lem2  35167  kur14lem3  35168  kur14lem5  35170  kur14lem6  35171  txsconnlem  35200  cvmliftlem4  35248  cvmliftlem5  35249  satf0sucom  35333  satf0suc  35336  satf0op  35337  fmla  35341  satffunlem2lem2  35366  satfv0fvfmla0  35373  sate0  35375  funpartfv  35906  fullfunfv  35908  sumeq2si  36163  prodeq2si  36165  cbvprodvw2  36208  neibastop2lem  36321  dffinxpf  37346  ftc1cnnc  37659  heiborlem4  37781  heiborlem6  37783  cdlemk13  40819  cdlemk14  40821  cdlemk15  40822  cdlemk21N  40840  cdlemk20  40841  cdlemk56w  40940  lcfrlem1  41509  hdmapfval  41794  deg1gprod  42101  evlsevl  42532  selvvvval  42546  rabdiophlem2  42763  dnnumch1  43006  aomclem6  43021  mncn0  43101  aaitgo  43124  rngunsnply  43131  cytpval  43164  dssmapntrcls  44090  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  binomcxp  44319  fvcod  45194  fvmpt2df  45239  fsumsermpt  45550  fmul01  45551  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  lptioo2cn  45616  lptioo1cn  45617  limclner  45622  dvsinax  45884  fperdvper  45890  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  dvnprodlem3  45919  itgsin0pilem1  45921  stoweidlem3  45974  stoweidlem17  45988  stoweidlem47  46018  fourierdlem42  46120  fourierdlem62  46139  fourierdlem80  46157  fourierdlem90  46167  fourierdlem92  46169  fourierdlem93  46170  fourierdlem103  46180  fourierdlem104  46181  fouriercnp  46197  sge0isum  46398  sge0seq  46417  ovnsubadd  46543  vonn0ioo  46658  vonn0icc  46659  smflimsup  46799  cjnpoly  46863  sinnpoly  46865  fcores  47041  fundcmpsurinjimaid  47385  isgrim  47855  gricushgr  47890  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem6  48063  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem10  48067  rhmsubcALTVlem2  48243  ply1mulgsum  48352  lineval  48356  lincvalpr  48380  lindslinindimp2lem4  48423  zlmodzxzldeplem3  48464  zlmodzxzldeplem4  48465  itcoval0mpt  48628  ackvalsuc1mpt  48640  ackval0  48642  ackval40  48655  ackval41a  48656  ackval42  48658  ackval50  48660  ehl2eudisval0  48687  2sphere0  48712  line2  48714  line2x  48716  line2y  48717  itscnhlinecirc02p  48747  oppcup  49169  natoppf  49191