Theorem fveq1i 6757

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

Syntax hints:   = wceq 1539  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  fveq12i  6762  fvun2  6842  fvopab3ig  6853  fvsnun1  7036  fvpr1g  7044  fvpr2g  7045  fvpr2gOLD  7046  fvpr1OLD  7048  fvpr2OLD  7050  fvtp1  7052  fvtp2  7053  fvtp3  7054  fvtp1g  7055  fvtp2g  7056  fvtp3g  7057  fpropnf1  7121  fveqf1o  7155  ov  7395  ovigg  7396  ovg  7415  fvresex  7776  curry1  7915  curry2  7918  fsplitfpar  7930  suppsnop  7965  frrlem12  8084  fprlem1  8087  wfrlem5OLD  8115  tfr2a  8197  rdgsucmptf  8230  rdgsucmptnf  8231  frsucmpt  8239  frsucmptn  8240  seqomlem1  8251  seqomlem3  8253  seqomlem4  8254  seqom0g  8257  seqomsuc  8258  unblem2  8997  inf3lemb  9313  inf3lemc  9314  trpredmintr  9409  trpred0  9410  trcl  9417  frrlem15  9446  r10  9457  r1sucg  9458  r1limg  9460  infxpenc2  9709  aleph0  9753  alephlim  9754  alephsuc  9755  alephfplem1  9791  alephfplem2  9792  ackbij2lem3  9928  cfsmolem  9957  infpssrlem1  9990  infpssrlem2  9991  fin23lem34  10033  fin23lem35  10034  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  isf34lem5  10065  hsmexlem7  10110  axdclem2  10207  canthp1lem2  10340  wunex2  10425  wuncval2  10434  addpiord  10571  mulpiord  10572  addpqnq  10625  mulpqnq  10628  fseq1p1m1  13259  om2uz0i  13595  om2uzrdg  13604  uzrdg0i  13607  uzrdgsuci  13608  hashkf  13974  hashgval  13975  hashinf  13977  ccat1st1st  14263  revs1  14406  cats1fv  14500  shftidt  14721  cbvsum  15335  fsumss  15365  isumclim3  15399  isumsup2  15486  cbvprod  15553  fprodss  15586  iprodclim3  15638  fprodefsum  15732  ruclem4  15871  ruclem6  15872  ruclem7  15873  sadc0  16089  sadcp1  16090  sadcaddlem  16092  sadaddlem  16101  smup0  16114  smupp1  16115  algr0  16205  algrp1  16207  ndxarg  16825  strfv2d  16831  funcoppc  17506  fthepi  17560  homadm  17671  homacd  17672  prdsidlem  18332  prdsinvlem  18599  cayleylem2  18936  symggen  18993  pmtr3ncomlem1  18996  gsumval3  19423  gsumzaddlem  19437  gsumzmhm  19453  pgpfaclem1  19599  ringidval  19654  lidlval  20375  rspval  20376  lidlnegcl  20398  lpival  20429  znf1o  20671  eqcoe1ply1eq  21378  evls1val  21396  evl1val  21405  mat1dimmul  21533  mdetralt  21665  mdetunilem7  21675  decpmatid  21827  pmatcollpwscmatlem1  21846  cpmidpmat  21930  chcoeffeq  21943  restcls  22240  restntr  22241  upxp  22682  cnmetdval  23840  remetdval  23858  qdensere2  23866  pcoptcl  24090  pcopt  24091  pcopt2  24092  pcorevlem  24095  isncvsngp  24218  cnncvsabsnegdemo  24234  ovolfsval  24539  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliun2  24575  ovolscalem1  24582  ovolicc2lem4  24589  mblvol  24599  ioombl1lem4  24630  uniioovol  24648  uniioombllem3  24654  0pval  24740  limccnp  24960  limccnp2  24961  dvcnvrelem2  25087  itgsubstlem  25117  ply1remlem  25232  plyrem  25370  qaa  25388  abelth  25505  efif1olem4  25606  eflog  25637  logef  25642  logeftb  25644  dvrelog  25697  dvlog  25711  cxpcn3  25806  efrlim  26024  eflgam  26099  wilthlem3  26124  basellem8  26142  lgsqrlem1  26399  tgcgr4  26796  krippenlem  26955  colperpexlem1  26995  opphllem3  27014  lmiisolem  27061  axlowdimlem8  27220  axlowdimlem9  27221  axlowdimlem11  27223  axlowdimlem12  27224  axlowdimlem17  27229  ushgredgedg  27499  ushgredgedgloop  27501  subgruhgredgd  27554  vtxdlfgrval  27755  vtxd0nedgb  27758  vtxdushgrfvedg  27760  vtxdginducedm1lem3  27811  finsumvtxdg2size  27820  vtxdgoddnumeven  27823  isrgr  27829  fusgrregdegfi  27839  wlk1walk  27908  wlkres  27940  wlkp1lem5  27947  wlkp1lem6  27948  wlkp1lem7  27949  wlkp1lem8  27950  clwlkcompbp  28051  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  2wlkdlem3  28193  2wlkdlem8  28199  2wlkond  28203  umgr2adedgwlk  28211  1wlkdlem4  28405  1pthond  28409  wlk2v2elem2  28421  3wlkdlem3  28426  3wlkdlem8  28432  3cycld  28443  3cyclpd  28444  eucrctshift  28508  frgrncvvdeq  28574  frgrwopreglem2  28578  ex-fpar  28727  avril1  28728  vafval  28866  smfval  28868  0vfval  28869  nmcvfval  28870  vsfval  28896  hhssabloilem  29524  pjoc2i  29701  pjcji  29947  ho0val  30013  hoival  30018  adjbdlnb  30347  nmopcoadji  30364  opsqrlem2  30404  opsqrlem5  30407  hmopidmchi  30414  hmopidmpji  30415  pjinvari  30454  pjadj2coi  30467  pj3lem1  30469  funcnvmpt  30906  pmtrprfv2  31259  cycpmco2lem7  31301  rgmoddim  31595  madjusmdetlem1  31679  cnre2csqlem  31762  zzsnm  31811  rrhcn  31847  qqhre  31870  oms0  32164  omsmon  32165  omssubaddlem  32166  omssubadd  32167  eulerpart  32249  fib0  32266  fib1  32267  fibp1  32268  coinflippv  32350  gsumnunsn  32420  2cycld  33000  derangenlem  33033  kur14lem2  33069  kur14lem3  33070  kur14lem5  33072  kur14lem6  33073  txsconnlem  33102  cvmliftlem4  33150  cvmliftlem5  33151  satf0sucom  33235  satf0suc  33238  satf0op  33239  fmla  33243  satffunlem2lem2  33268  satfv0fvfmla0  33275  sate0  33277  ttrclselem1  33711  ttrclselem2  33712  noetasuplem4  33866  noetainflem4  33870  funpartfv  34174  fullfunfv  34176  neibastop2lem  34476  dffinxpf  35483  ftc1cnnc  35776  heiborlem4  35899  heiborlem6  35901  cdlemk13  38793  cdlemk14  38795  cdlemk15  38796  cdlemk21N  38814  cdlemk20  38815  cdlemk56w  38914  lcfrlem1  39483  hdmapfval  39768  rabdiophlem2  40540  dnnumch1  40785  aomclem6  40800  mncn0  40880  aaitgo  40903  rngunsnply  40914  cytpval  40950  dssmapntrcls  41627  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  binomcxp  41864  fvcod  42655  fsumsermpt  43010  fmul01  43011  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  lptioo2cn  43076  lptioo1cn  43077  limclner  43082  dvsinax  43344  fperdvper  43350  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  itgsin0pilem1  43381  stoweidlem3  43434  stoweidlem17  43448  stoweidlem47  43478  fourierdlem42  43580  fourierdlem62  43599  fourierdlem80  43617  fourierdlem90  43627  fourierdlem92  43629  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fouriercnp  43657  sge0isum  43855  sge0seq  43874  ovnsubadd  44000  vonn0ioo  44115  vonn0icc  44116  smflimsup  44248  fcores  44448  fundcmpsurinjimaid  44751  isomushgr  45166  rhmsubclem2  45533  rhmsubcALTVlem2  45551  ply1mulgsum  45619  lineval  45623  lincvalpr  45647  lindslinindimp2lem4  45690  zlmodzxzldeplem3  45731  zlmodzxzldeplem4  45732  itcoval0mpt  45900  ackvalsuc1mpt  45912  ackval0  45914  ackval40  45927  ackval41a  45928  ackval42  45930  ackval50  45932  ehl2eudisval0  45959  2sphere0  45984  line2  45986  line2x  45988  line2y  45989  itscnhlinecirc02p  46019