Theorem fveq1i 6863

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

Syntax hints:   = wceq 1559  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524

This theorem is referenced by:  fveq12i  6868  fvun2  6954  fvcod  6961  fvopab3ig  6966  funcnvmpt  6972  fvsnun1  7161  fvpr1g  7169  fvpr2g  7170  fvtp1  7174  fvtp2  7175  fvtp3  7176  fvtp1g  7177  fvtp2g  7178  fvtp3g  7179  fpropnf1  7246  fveqf1o  7281  ov  7535  ovigg  7536  ovg  7556  fvresex  7936  curry1  8077  curry2  8080  fsplitfpar  8091  suppsnop  8152  frrlem12  8272  fprlem1  8275  tfr2a  8360  rdgsucmptf  8393  rdgsucmptnf  8394  frsucmpt  8403  frsucmptn  8404  seqomlem1  8415  seqomlem3  8417  seqomlem4  8418  seqom0g  8421  seqomsuc  8422  unblem2  9231  inf3lemb  9574  inf3lemc  9575  ttrclselem1  9674  ttrclselem2  9675  trcl  9677  frrlem15  9709  r10  9720  r1sucg  9721  r1limg  9723  infxpenc2  9972  aleph0  10016  alephlim  10017  alephsuc  10018  alephfplem1  10054  alephfplem2  10055  ackbij2lem3  10190  cfsmolem  10221  infpssrlem1  10254  infpssrlem2  10255  fin23lem34  10297  fin23lem35  10298  isf32lem6  10309  isf32lem7  10310  isf32lem8  10311  isf34lem5  10329  hsmexlem7  10374  axdclem2  10471  canthp1lem2  10605  wunex2  10690  wuncval2  10699  addpiord  10836  mulpiord  10837  addpqnq  10890  mulpqnq  10893  fseq1p1m1  13597  om2uz0i  13954  om2uzrdg  13963  uzrdg0i  13966  uzrdgsuci  13967  hashkf  14339  hashgval  14340  hashinf  14342  ccat1st1st  14636  revs1  14772  cats1fv  14866  shftidt  15089  cbvsum  15713  cbvsumv  15714  fsumss  15743  isumclim3  15777  indsumhash  15848  isumsup2  15867  cbvprod  15934  cbvprodv  15935  fprodss  15969  iprodclim3  16021  fprodefsum  16116  ruclem4  16257  ruclem6  16258  ruclem7  16259  sadc0  16479  sadcp1  16480  sadcaddlem  16482  sadaddlem  16491  smup0  16504  smupp1  16505  algr0  16597  algrp1  16599  ndxarg  17223  strfv2d  17228  funcoppc  17899  fthepi  17954  homadm  18064  homacd  18065  prdsidlem  18794  prdsinvlem  19082  cayleylem2  19444  symggen  19501  pmtr3ncomlem1  19504  gsumval3  19938  gsumzaddlem  19952  gsumzmhm  19968  pgpfaclem1  20114  ringidval  20220  rhmsubclem2  20723  lidlval  21268  rspval  21269  lidlnegcl  21280  lpival  21382  znf1o  21591  evlsevl  22173  selvvvval  22183  ply1ascl0  22304  ply1ascl1  22305  eqcoe1ply1eq  22350  evls1val  22371  evl1val  22380  mat1dimmul  22524  mdetralt  22656  mdetunilem7  22666  decpmatid  22818  pmatcollpwscmatlem1  22837  cpmidpmat  22921  chcoeffeq  22934  restcls  23229  restntr  23230  upxp  23671  cnmetdval  24818  remetdval  24837  qdensere2  24845  pcoptcl  25071  pcopt  25072  pcopt2  25073  pcorevlem  25076  isncvsngp  25199  cnncvsabsnegdemo  25215  ovolfsval  25520  ovollb2lem  25538  ovolunlem1a  25546  ovoliunlem1  25552  ovoliun2  25556  ovolscalem1  25563  ovolicc2lem4  25570  mblvol  25580  ioombl1lem4  25611  uniioovol  25629  uniioombllem3  25635  0pval  25721  limccnp  25941  limccnp2  25942  dvcnvrelem2  26068  itgsubstlem  26098  ply1remlem  26213  plyrem  26357  qaa  26375  abelth  26492  efif1olem4  26598  eflog  26629  logef  26634  logeftb  26636  dvrelog  26690  dvlog  26704  cxpcn3  26801  efrlim  27022  eflgam  27097  wilthlem3  27122  basellem8  27140  lgsqrlem1  27398  noetasuplem4  27788  noetainflem4  27792  precsexlem1  28288  precsexlem2  28289  precsexlem3  28290  precsexlem4  28291  precsexlem5  28292  tgcgr4  28688  krippenlem  28847  colperpexlem1  28887  opphllem3  28906  lmiisolem  28953  axlowdimlem8  29107  axlowdimlem9  29108  axlowdimlem11  29110  axlowdimlem12  29111  axlowdimlem17  29116  ushgredgedg  29387  ushgredgedgloop  29389  subgruhgredgd  29442  vtxdlfgrval  29643  vtxd0nedgb  29646  vtxdushgrfvedg  29648  vtxdginducedm1lem3  29699  finsumvtxdg2size  29708  vtxdgoddnumeven  29711  isrgr  29717  fusgrregdegfi  29727  wlk1walk  29796  wlkres  29826  wlkp1lem5  29833  wlkp1lem6  29834  wlkp1lem7  29835  wlkp1lem8  29836  clwlkcompbp  29939  crctcshwlkn0lem4  29970  crctcshwlkn0lem5  29971  crctcshwlkn0lem6  29972  2wlkdlem3  30084  2wlkdlem8  30090  2wlkond  30094  umgr2adedgwlk  30102  1wlkdlem4  30299  1pthond  30303  wlk2v2elem2  30315  3wlkdlem3  30320  3wlkdlem8  30326  3cycld  30337  3cyclpd  30338  eucrctshift  30402  frgrncvvdeq  30468  frgrwopreglem2  30472  ex-fpar  30621  avril1  30622  vafval  30763  smfval  30765  0vfval  30766  nmcvfval  30767  vsfval  30793  hhssabloilem  31421  pjoc2i  31598  pjcji  31844  ho0val  31910  hoival  31915  adjbdlnb  32244  nmopcoadji  32261  opsqrlem2  32301  opsqrlem5  32304  hmopidmchi  32311  hmopidmpji  32312  pjinvari  32351  pjadj2coi  32364  pj3lem1  32366  pmtrprfv2  33229  cycpmco2lem7  33273  evl1fpws  33721  mplmulmvr  33797  evlextv  33800  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  esplyindfv  33834  esplyfvn  33835  vietalem  33837  rtelextdg2lem  33984  constr0  33995  constrsuc  33996  constrlim  33997  2sqr3minply  34038  cos9thpiminplylem6  34045  madjusmdetlem1  34085  cnre2csqlem  34168  zzsnm  34217  rrhcn  34255  qqhre  34278  oms0  34555  omsmon  34556  omssubaddlem  34557  omssubadd  34558  eulerpart  34640  fib0  34657  fib1  34658  fibp1  34659  coinflippv  34742  gsumnunsn  34799  2cycld  35449  derangenlem  35482  kur14lem2  35518  kur14lem3  35519  kur14lem5  35521  kur14lem6  35522  txsconnlem  35551  cvmliftlem4  35599  cvmliftlem5  35600  satf0sucom  35684  satf0suc  35687  satf0op  35688  fmla  35692  satffunlem2lem2  35717  satfv0fvfmla0  35724  sate0  35726  funpartfv  36256  fullfunfv  36258  sumeq2si  36523  prodeq2si  36525  cbvprodvw2  36568  neibastop2lem  36681  dffinxpf  37840  ftc1cnnc  38152  heiborlem4  38274  heiborlem6  38276  cdlemk13  41437  cdlemk14  41439  cdlemk15  41440  cdlemk21N  41458  cdlemk20  41459  cdlemk56w  41558  lcfrlem1  42127  hdmapfval  42412  deg1gprod  42718  rabdiophlem2  43340  dnnumch1  43582  aomclem6  43597  mncn0  43677  aaitgo  43700  rngunsnply  43707  cytpval  43740  dssmapntrcls  44665  binomcxplemdvsum  44892  binomcxplemnotnn0  44893  binomcxp  44894  fvmpt2df  45808  fsumsermpt  46116  fmul01  46117  fmuldfeq  46120  fmul01lt1lem1  46121  fmul01lt1lem2  46122  lptioo2cn  46180  lptioo1cn  46181  limclner  46186  dvsinax  46448  fperdvper  46454  dvnmul  46478  dvnprodlem1  46481  dvnprodlem2  46482  dvnprodlem3  46483  itgsin0pilem1  46485  stoweidlem3  46538  stoweidlem17  46552  stoweidlem47  46582  fourierdlem42  46684  fourierdlem62  46703  fourierdlem80  46721  fourierdlem90  46731  fourierdlem92  46733  fourierdlem93  46734  fourierdlem103  46744  fourierdlem104  46745  fouriercnp  46761  sge0isum  46962  sge0seq  46981  ovnsubadd  47107  vonn0ioo  47222  vonn0icc  47223  smflimsup  47363  cjnpoly  47444  sinnpoly  47446  fcores  47622  fundcmpsurinjimaid  47978  isgrim  48465  gricushgr  48500  gpgprismgr4cycllem3  48680  gpgprismgr4cycllem6  48683  gpgprismgr4cycllem7  48684  gpgprismgr4cycllem10  48687  rhmsubcALTVlem2  48865  ply1mulgsum  48973  lineval  48977  lincvalpr  49001  lindslinindimp2lem4  49044  zlmodzxzldeplem3  49085  zlmodzxzldeplem4  49086  itcoval0mpt  49249  ackvalsuc1mpt  49261  ackval0  49263  ackval40  49276  ackval41a  49277  ackval42  49279  ackval50  49281  ehl2eudisval0  49308  2sphere0  49333  line2  49335  line2x  49337  line2y  49338  itscnhlinecirc02p  49368  oppcup  49789  natoppf  49811