Theorem fveq1i 6104

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

Syntax hints:   = wceq 1475  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812

This theorem is referenced by:  fveq12i  6108  fvun2  6180  fvopab3ig  6188  fvsnun1  6353  fvsnun2  6354  fvpr1  6361  fvpr2  6362  fvpr1g  6363  fvpr2g  6364  fvtp1  6365  fvtp2  6366  fvtp3  6367  fvtp1g  6368  fvtp2g  6369  fvtp3g  6370  fveqf1o  6457  ov  6678  ovigg  6679  ovg  6697  fvresex  7032  curry1  7156  curry2  7159  suppsnop  7196  wfrlem5  7306  tfr2a  7378  rdgsucmptf  7411  rdgsucmptnf  7412  frsucmpt  7420  frsucmptn  7421  seqomlem1  7432  seqomlem3  7434  seqomlem4  7435  seqom0g  7438  seqomsuc  7439  unblem2  8098  inf3lemb  8405  inf3lemc  8406  trcl  8487  r10  8514  r1sucg  8515  r1limg  8517  infxpenc2  8728  aleph0  8772  alephlim  8773  alephsuc  8774  alephfplem1  8810  alephfplem2  8811  ackbij2lem3  8946  cfsmolem  8975  infpssrlem1  9008  infpssrlem2  9009  fin23lem34  9051  fin23lem35  9052  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  isf34lem5  9083  hsmexlem7  9128  axdclem2  9225  canthp1lem2  9354  wunex2  9439  wuncval2  9448  addpiord  9585  mulpiord  9586  addpqnq  9639  mulpqnq  9642  fseq1p1m1  12283  om2uz0i  12608  om2uzrdg  12617  uzrdg0i  12620  uzrdgsuci  12621  hashkf  12981  hashgval  12982  hashinf  12984  revs1  13365  cats1fv  13455  shftidt  13670  cbvsum  14273  fsumss  14303  isumclim3  14332  isumsup2  14417  cbvprod  14484  fprodss  14517  iprodclim3  14570  fprodefsum  14664  ruclem4  14802  ruclem6  14803  ruclem7  14804  sadc0  15014  sadcp1  15015  sadcaddlem  15017  sadaddlem  15026  smup0  15039  smupp1  15040  algr0  15123  algrp1  15125  ndxarg  15715  strfv2d  15733  xpsc0  16043  xpsc1  16044  funcoppc  16358  fthepi  16411  homadm  16513  homacd  16514  prdsidlem  17145  prdsinvlem  17347  cayleylem2  17656  symggen  17713  pmtr3ncomlem1  17716  gsumval3  18131  gsumzaddlem  18144  gsumzmhm  18160  pgpfaclem1  18303  ringidval  18326  lidlval  19013  rspval  19014  lidlnegcl  19035  lpival  19066  eqcoe1ply1eq  19488  evls1val  19506  evl1val  19514  znf1o  19719  mat1dimmul  20101  mdetralt  20233  mdetunilem7  20243  decpmatid  20394  pmatcollpwscmatlem1  20413  cpmidpmat  20497  chcoeffeq  20510  restcls  20795  restntr  20796  upxp  21236  cnmetdval  22384  remetdval  22400  qdensere2  22408  pcoptcl  22629  pcopt  22630  pcopt2  22631  pcorevlem  22634  isncvsngp  22757  cnncvsabsnegdemo  22773  ovolfsval  23046  ovollb2lem  23063  ovolunlem1a  23071  ovoliunlem1  23077  ovoliun2  23081  ovolscalem1  23088  ovolicc2lem4  23095  mblvol  23105  ioombl1lem4  23136  uniioovol  23153  uniioombllem3  23159  0pval  23244  limccnp  23461  limccnp2  23462  dvcnvrelem2  23585  itgsubstlem  23615  ply1remlem  23726  plyrem  23864  qaa  23882  abelth  23999  efif1olem4  24095  eflog  24127  logef  24132  logeftb  24134  dvrelog  24183  dvlog  24197  cxpcn3  24289  efrlim  24496  eflgam  24571  wilthlem3  24596  basellem8  24614  lgsqrlem1  24871  tgcgr4  25226  krippenlem  25385  colperpexlem1  25422  opphllem3  25441  lmiisolem  25488  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem11  25632  axlowdimlem12  25633  axlowdimlem17  25638  2wlklemA  26084  2wlklemB  26085  2wlklemC  26086  wlkntrllem2  26090  wlkntrllem3  26091  constr3lem4  26175  constr3lem5  26176  wlkiswwlksur  26247  vdgr1c  26432  eupares  26502  eupap1  26503  vdegp1ai  26511  vdegp1bi  26512  avril1  26711  vafval  26842  smfval  26844  0vfval  26845  nmcvfval  26846  vsfval  26872  hhssabloilem  27502  pjoc2i  27681  pjcji  27927  ho0val  27993  hoival  27998  adjbdlnb  28327  nmopcoadji  28344  opsqrlem2  28384  opsqrlem5  28387  hmopidmchi  28394  hmopidmpji  28395  pjinvari  28434  pjadj2coi  28447  pj3lem1  28449  funcnvmptOLD  28850  funcnvmpt  28851  pmtrprfv2  29179  madjusmdetlem1  29221  cnre2csqlem  29284  zzsnm  29333  rrhcn  29369  qqhre  29392  oms0  29686  omsmon  29687  omssubaddlem  29688  omssubadd  29689  eulerpart  29771  fib0  29788  fib1  29789  fibp1  29790  coinflippv  29872  gsumnunsn  29942  derangenlem  30407  kur14lem2  30443  kur14lem3  30444  kur14lem5  30446  kur14lem6  30447  txsconlem  30476  cvmliftlem4  30524  cvmliftlem5  30525  trpredmintr  30975  trpred0  30980  frrlem5  31028  funpartfv  31222  fullfunfv  31224  neibastop2lem  31525  dffinxpf  32398  ftc1cnnc  32654  heiborlem4  32783  heiborlem6  32785  cdlemk13  35158  cdlemk14  35160  cdlemk15  35161  cdlemk21N  35179  cdlemk20  35180  cdlemk56w  35279  lcfrlem1  35849  hdmapfval  36137  rabdiophlem2  36384  dnnumch1  36632  aomclem6  36647  mncn0  36728  aaitgo  36751  rngunsnply  36762  cytpval  36806  dssmapntrcls  37446  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  binomcxp  37578  fvcod  38418  fsumsermpt  38646  fmul01  38647  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  lptioo2cn  38712  lptioo1cn  38713  limclner  38718  dvsinax  38801  fperdvper  38808  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  itgsin0pilem1  38841  stoweidlem3  38896  stoweidlem17  38910  stoweidlem47  38940  fourierdlem42  39042  fourierdlem62  39061  fourierdlem80  39079  fourierdlem90  39089  fourierdlem92  39091  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fouriercnp  39119  sge0isum  39320  sge0seq  39339  ovnsubadd  39462  vonn0ioo  39578  vonn0icc  39579  fpropnf1  40337  ushgredgedga  40456  ushgredgedgaloop  40458  subgruhgredgd  40508  vtxdlfgrval  40700  vtxd0nedgb  40703  vtxdushgrfvedg  40705  isrgr  40759  fusgrregdegfi  40769  1wlk1walk  40843  1wlkres  40879  1wlkp1lem5  40886  1wlkp1lem6  40887  1wlkp1lem7  40888  1wlkp1lem8  40889  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  wlkwwlksur  41094  21wlkdlem3  41134  21wlkdlem8  41140  21wlkond  41144  umgr2adedgwlk  41152  11wlkdlem4  41307  1pthond  41311  1wlk2v2elem2  41323  31wlkdlem3  41328  31wlkdlem8  41334  3cycld  41345  3cyclpd  41346  eucrctshift  41411  frgrncvvdeq  41480  frgrwopreglem2  41482  rhmsubclem2  41879  rhmsubcALTVlem2  41898  ply1mulgsum  41972  lineval  41976  lincvalpr  42001  lindslinindimp2lem4  42044  zlmodzxzldeplem3  42085  zlmodzxzldeplem4  42086