Theorem fveq1i 6876

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

Syntax hints:   = wceq 1540  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  fveq12i  6881  fvun2  6970  fvopab3ig  6981  fvsnun1  7173  fvpr1g  7181  fvpr2g  7182  fvtp1  7186  fvtp2  7187  fvtp3  7188  fvtp1g  7189  fvtp2g  7190  fvtp3g  7191  fpropnf1  7259  fveqf1o  7294  ov  7549  ovigg  7550  ovg  7570  fvresex  7956  curry1  8101  curry2  8104  fsplitfpar  8115  suppsnop  8175  frrlem12  8294  fprlem1  8297  wfrlem5OLD  8325  tfr2a  8407  rdgsucmptf  8440  rdgsucmptnf  8441  frsucmpt  8450  frsucmptn  8451  seqomlem1  8462  seqomlem3  8464  seqomlem4  8465  seqom0g  8468  seqomsuc  8469  unblem2  9299  inf3lemb  9637  inf3lemc  9638  ttrclselem1  9737  ttrclselem2  9738  trcl  9740  frrlem15  9769  r10  9780  r1sucg  9781  r1limg  9783  infxpenc2  10034  aleph0  10078  alephlim  10079  alephsuc  10080  alephfplem1  10116  alephfplem2  10117  ackbij2lem3  10252  cfsmolem  10282  infpssrlem1  10315  infpssrlem2  10316  fin23lem34  10358  fin23lem35  10359  isf32lem6  10370  isf32lem7  10371  isf32lem8  10372  isf34lem5  10390  hsmexlem7  10435  axdclem2  10532  canthp1lem2  10665  wunex2  10750  wuncval2  10759  addpiord  10896  mulpiord  10897  addpqnq  10950  mulpqnq  10953  fseq1p1m1  13613  om2uz0i  13963  om2uzrdg  13972  uzrdg0i  13975  uzrdgsuci  13976  hashkf  14348  hashgval  14349  hashinf  14351  ccat1st1st  14644  revs1  14781  cats1fv  14876  shftidt  15099  cbvsum  15709  cbvsumv  15710  fsumss  15739  isumclim3  15773  isumsup2  15860  cbvprod  15927  cbvprodv  15928  fprodss  15962  iprodclim3  16014  fprodefsum  16109  ruclem4  16250  ruclem6  16251  ruclem7  16252  sadc0  16471  sadcp1  16472  sadcaddlem  16474  sadaddlem  16483  smup0  16496  smupp1  16497  algr0  16589  algrp1  16591  ndxarg  17213  strfv2d  17218  funcoppc  17886  fthepi  17941  homadm  18051  homacd  18052  prdsidlem  18745  prdsinvlem  19030  cayleylem2  19392  symggen  19449  pmtr3ncomlem1  19452  gsumval3  19886  gsumzaddlem  19900  gsumzmhm  19916  pgpfaclem1  20062  ringidval  20141  rhmsubclem2  20644  lidlval  21169  rspval  21170  lidlnegcl  21181  lpival  21283  znf1o  21510  ply1ascl0  22188  ply1ascl1  22189  eqcoe1ply1eq  22235  evls1val  22256  evl1val  22265  mat1dimmul  22412  mdetralt  22544  mdetunilem7  22554  decpmatid  22706  pmatcollpwscmatlem1  22725  cpmidpmat  22809  chcoeffeq  22822  restcls  23117  restntr  23118  upxp  23559  cnmetdval  24707  remetdval  24726  qdensere2  24734  pcoptcl  24970  pcopt  24971  pcopt2  24972  pcorevlem  24975  isncvsngp  25099  cnncvsabsnegdemo  25115  ovolfsval  25421  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliun2  25457  ovolscalem1  25464  ovolicc2lem4  25471  mblvol  25481  ioombl1lem4  25512  uniioovol  25530  uniioombllem3  25536  0pval  25622  limccnp  25842  limccnp2  25843  dvcnvrelem2  25973  itgsubstlem  26005  ply1remlem  26120  plyrem  26263  qaa  26281  abelth  26401  efif1olem4  26504  eflog  26535  logef  26540  logeftb  26542  dvrelog  26596  dvlog  26610  cxpcn3  26708  efrlim  26929  efrlimOLD  26930  eflgam  27005  wilthlem3  27030  basellem8  27048  lgsqrlem1  27307  noetasuplem4  27698  noetainflem4  27702  precsexlem1  28148  precsexlem2  28149  precsexlem3  28150  precsexlem4  28151  precsexlem5  28152  tgcgr4  28456  krippenlem  28615  colperpexlem1  28655  opphllem3  28674  lmiisolem  28721  axlowdimlem8  28874  axlowdimlem9  28875  axlowdimlem11  28877  axlowdimlem12  28878  axlowdimlem17  28883  ushgredgedg  29154  ushgredgedgloop  29156  subgruhgredgd  29209  vtxdlfgrval  29411  vtxd0nedgb  29414  vtxdushgrfvedg  29416  vtxdginducedm1lem3  29467  finsumvtxdg2size  29476  vtxdgoddnumeven  29479  isrgr  29485  fusgrregdegfi  29495  wlk1walk  29565  wlkres  29596  wlkp1lem5  29603  wlkp1lem6  29604  wlkp1lem7  29605  wlkp1lem8  29606  clwlkcompbp  29710  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshwlkn0lem6  29743  2wlkdlem3  29855  2wlkdlem8  29861  2wlkond  29865  umgr2adedgwlk  29873  1wlkdlem4  30067  1pthond  30071  wlk2v2elem2  30083  3wlkdlem3  30088  3wlkdlem8  30094  3cycld  30105  3cyclpd  30106  eucrctshift  30170  frgrncvvdeq  30236  frgrwopreglem2  30240  ex-fpar  30389  avril1  30390  vafval  30530  smfval  30532  0vfval  30533  nmcvfval  30534  vsfval  30560  hhssabloilem  31188  pjoc2i  31365  pjcji  31611  ho0val  31677  hoival  31682  adjbdlnb  32011  nmopcoadji  32028  opsqrlem2  32068  opsqrlem5  32071  hmopidmchi  32078  hmopidmpji  32079  pjinvari  32118  pjadj2coi  32131  pj3lem1  32133  funcnvmpt  32591  pmtrprfv2  33045  cycpmco2lem7  33089  evl1fpws  33523  rgmoddimOLD  33596  rtelextdg2lem  33706  constr0  33717  constrsuc  33718  constrlim  33719  2sqr3minply  33760  cos9thpiminplylem6  33767  madjusmdetlem1  33804  cnre2csqlem  33887  zzsnm  33936  rrhcn  33974  qqhre  33997  oms0  34275  omsmon  34276  omssubaddlem  34277  omssubadd  34278  eulerpart  34360  fib0  34377  fib1  34378  fibp1  34379  coinflippv  34462  gsumnunsn  34519  2cycld  35106  derangenlem  35139  kur14lem2  35175  kur14lem3  35176  kur14lem5  35178  kur14lem6  35179  txsconnlem  35208  cvmliftlem4  35256  cvmliftlem5  35257  satf0sucom  35341  satf0suc  35344  satf0op  35345  fmla  35349  satffunlem2lem2  35374  satfv0fvfmla0  35381  sate0  35383  funpartfv  35909  fullfunfv  35911  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36211  neibastop2lem  36324  dffinxpf  37349  ftc1cnnc  37662  heiborlem4  37784  heiborlem6  37786  cdlemk13  40817  cdlemk14  40819  cdlemk15  40820  cdlemk21N  40838  cdlemk20  40839  cdlemk56w  40938  lcfrlem1  41507  hdmapfval  41792  deg1gprod  42099  evlsevl  42541  selvvvval  42555  rabdiophlem2  42772  dnnumch1  43015  aomclem6  43030  mncn0  43110  aaitgo  43133  rngunsnply  43140  cytpval  43173  dssmapntrcls  44099  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  binomcxp  44329  fvcod  45199  fvmpt2df  45244  fsumsermpt  45556  fmul01  45557  fmuldfeq  45560  fmul01lt1lem1  45561  fmul01lt1lem2  45562  lptioo2cn  45622  lptioo1cn  45623  limclner  45628  dvsinax  45890  fperdvper  45896  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  itgsin0pilem1  45927  stoweidlem3  45980  stoweidlem17  45994  stoweidlem47  46024  fourierdlem42  46126  fourierdlem62  46145  fourierdlem80  46163  fourierdlem90  46173  fourierdlem92  46175  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  fouriercnp  46203  sge0isum  46404  sge0seq  46423  ovnsubadd  46549  vonn0ioo  46664  vonn0icc  46665  smflimsup  46805  fcores  47044  fundcmpsurinjimaid  47373  isgrim  47843  gricushgr  47878  gpgprismgr4cycllem3  48044  gpgprismgr4cycllem6  48047  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem10  48051  rhmsubcALTVlem2  48205  ply1mulgsum  48314  lineval  48318  lincvalpr  48342  lindslinindimp2lem4  48385  zlmodzxzldeplem3  48426  zlmodzxzldeplem4  48427  itcoval0mpt  48594  ackvalsuc1mpt  48606  ackval0  48608  ackval40  48621  ackval41a  48622  ackval42  48624  ackval50  48626  ehl2eudisval0  48653  2sphere0  48678  line2  48680  line2x  48682  line2y  48683  itscnhlinecirc02p  48713  oppcup  49057