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 1542  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  fveq12i  6846  fvun2  6932  fvopab3ig  6943  funcnvmpt  6949  fvsnun1  7137  fvpr1g  7145  fvpr2g  7146  fvtp1  7150  fvtp2  7151  fvtp3  7152  fvtp1g  7153  fvtp2g  7154  fvtp3g  7155  fpropnf1  7222  fveqf1o  7257  ov  7511  ovigg  7512  ovg  7532  fvresex  7913  curry1  8054  curry2  8057  fsplitfpar  8068  suppsnop  8128  frrlem12  8247  fprlem1  8250  tfr2a  8334  rdgsucmptf  8367  rdgsucmptnf  8368  frsucmpt  8377  frsucmptn  8378  seqomlem1  8389  seqomlem3  8391  seqomlem4  8392  seqom0g  8395  seqomsuc  8396  unblem2  9203  inf3lemb  9546  inf3lemc  9547  ttrclselem1  9646  ttrclselem2  9647  trcl  9649  frrlem15  9681  r10  9692  r1sucg  9693  r1limg  9695  infxpenc2  9944  aleph0  9988  alephlim  9989  alephsuc  9990  alephfplem1  10026  alephfplem2  10027  ackbij2lem3  10162  cfsmolem  10192  infpssrlem1  10225  infpssrlem2  10226  fin23lem34  10268  fin23lem35  10269  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  isf34lem5  10300  hsmexlem7  10345  axdclem2  10442  canthp1lem2  10576  wunex2  10661  wuncval2  10670  addpiord  10807  mulpiord  10808  addpqnq  10861  mulpqnq  10864  fseq1p1m1  13552  om2uz0i  13909  om2uzrdg  13918  uzrdg0i  13921  uzrdgsuci  13922  hashkf  14294  hashgval  14295  hashinf  14297  ccat1st1st  14591  revs1  14727  cats1fv  14821  shftidt  15044  cbvsum  15657  cbvsumv  15658  fsumss  15687  isumclim3  15721  indsumhash  15792  isumsup2  15811  cbvprod  15878  cbvprodv  15879  fprodss  15913  iprodclim3  15965  fprodefsum  16060  ruclem4  16201  ruclem6  16202  ruclem7  16203  sadc0  16423  sadcp1  16424  sadcaddlem  16426  sadaddlem  16435  smup0  16448  smupp1  16449  algr0  16541  algrp1  16543  ndxarg  17166  strfv2d  17171  funcoppc  17842  fthepi  17897  homadm  18007  homacd  18008  prdsidlem  18737  prdsinvlem  19025  cayleylem2  19388  symggen  19445  pmtr3ncomlem1  19448  gsumval3  19882  gsumzaddlem  19896  gsumzmhm  19912  pgpfaclem1  20058  ringidval  20164  rhmsubclem2  20663  lidlval  21208  rspval  21209  lidlnegcl  21220  lpival  21322  znf1o  21531  ply1ascl0  22218  ply1ascl1  22219  eqcoe1ply1eq  22264  evls1val  22285  evl1val  22294  mat1dimmul  22441  mdetralt  22573  mdetunilem7  22583  decpmatid  22735  pmatcollpwscmatlem1  22754  cpmidpmat  22838  chcoeffeq  22851  restcls  23146  restntr  23147  upxp  23588  cnmetdval  24735  remetdval  24754  qdensere2  24762  pcoptcl  24988  pcopt  24989  pcopt2  24990  pcorevlem  24993  isncvsngp  25116  cnncvsabsnegdemo  25132  ovolfsval  25437  ovollb2lem  25455  ovolunlem1a  25463  ovoliunlem1  25469  ovoliun2  25473  ovolscalem1  25480  ovolicc2lem4  25487  mblvol  25497  ioombl1lem4  25528  uniioovol  25546  uniioombllem3  25552  0pval  25638  limccnp  25858  limccnp2  25859  dvcnvrelem2  25985  itgsubstlem  26015  ply1remlem  26130  plyrem  26271  qaa  26289  abelth  26406  efif1olem4  26509  eflog  26540  logef  26545  logeftb  26547  dvrelog  26601  dvlog  26615  cxpcn3  26712  efrlim  26933  eflgam  27008  wilthlem3  27033  basellem8  27051  lgsqrlem1  27309  noetasuplem4  27700  noetainflem4  27704  precsexlem1  28199  precsexlem2  28200  precsexlem3  28201  precsexlem4  28202  precsexlem5  28203  tgcgr4  28599  krippenlem  28758  colperpexlem1  28798  opphllem3  28817  lmiisolem  28864  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem11  29021  axlowdimlem12  29022  axlowdimlem17  29027  ushgredgedg  29298  ushgredgedgloop  29300  subgruhgredgd  29353  vtxdlfgrval  29554  vtxd0nedgb  29557  vtxdushgrfvedg  29559  vtxdginducedm1lem3  29610  finsumvtxdg2size  29619  vtxdgoddnumeven  29622  isrgr  29628  fusgrregdegfi  29638  wlk1walk  29707  wlkres  29737  wlkp1lem5  29744  wlkp1lem6  29745  wlkp1lem7  29746  wlkp1lem8  29747  clwlkcompbp  29850  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  2wlkdlem3  29995  2wlkdlem8  30001  2wlkond  30005  umgr2adedgwlk  30013  1wlkdlem4  30210  1pthond  30214  wlk2v2elem2  30226  3wlkdlem3  30231  3wlkdlem8  30237  3cycld  30248  3cyclpd  30249  eucrctshift  30313  frgrncvvdeq  30379  frgrwopreglem2  30383  ex-fpar  30532  avril1  30533  vafval  30674  smfval  30676  0vfval  30677  nmcvfval  30678  vsfval  30704  hhssabloilem  31332  pjoc2i  31509  pjcji  31755  ho0val  31821  hoival  31826  adjbdlnb  32155  nmopcoadji  32172  opsqrlem2  32212  opsqrlem5  32215  hmopidmchi  32222  hmopidmpji  32223  pjinvari  32262  pjadj2coi  32275  pj3lem1  32277  pmtrprfv2  33149  cycpmco2lem7  33193  evl1fpws  33624  mplmulmvr  33683  evlextv  33686  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vietalem  33723  rtelextdg2lem  33870  constr0  33881  constrsuc  33882  constrlim  33883  2sqr3minply  33924  cos9thpiminplylem6  33931  madjusmdetlem1  33971  cnre2csqlem  34054  zzsnm  34103  rrhcn  34141  qqhre  34164  oms0  34441  omsmon  34442  omssubaddlem  34443  omssubadd  34444  eulerpart  34526  fib0  34543  fib1  34544  fibp1  34545  coinflippv  34628  gsumnunsn  34685  2cycld  35320  derangenlem  35353  kur14lem2  35389  kur14lem3  35390  kur14lem5  35392  kur14lem6  35393  txsconnlem  35422  cvmliftlem4  35470  cvmliftlem5  35471  satf0sucom  35555  satf0suc  35558  satf0op  35559  fmla  35563  satffunlem2lem2  35588  satfv0fvfmla0  35595  sate0  35597  funpartfv  36127  fullfunfv  36129  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  neibastop2lem  36542  dffinxpf  37701  ftc1cnnc  38013  heiborlem4  38135  heiborlem6  38137  cdlemk13  41298  cdlemk14  41300  cdlemk15  41301  cdlemk21N  41319  cdlemk20  41320  cdlemk56w  41419  lcfrlem1  41988  hdmapfval  42273  deg1gprod  42579  evlsevl  43007  selvvvval  43018  rabdiophlem2  43230  dnnumch1  43472  aomclem6  43487  mncn0  43567  aaitgo  43590  rngunsnply  43597  cytpval  43630  dssmapntrcls  44555  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  binomcxp  44784  fvcod  45656  fvmpt2df  45701  fsumsermpt  46009  fmul01  46010  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  lptioo2cn  46073  lptioo1cn  46074  limclner  46079  dvsinax  46341  fperdvper  46347  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  itgsin0pilem1  46378  stoweidlem3  46431  stoweidlem17  46445  stoweidlem47  46475  fourierdlem42  46577  fourierdlem62  46596  fourierdlem80  46614  fourierdlem90  46624  fourierdlem92  46626  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fouriercnp  46654  sge0isum  46855  sge0seq  46874  ovnsubadd  47000  vonn0ioo  47115  vonn0icc  47116  smflimsup  47256  cjnpoly  47337  sinnpoly  47339  fcores  47515  fundcmpsurinjimaid  47871  isgrim  48358  gricushgr  48393  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem6  48576  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  rhmsubcALTVlem2  48758  ply1mulgsum  48866  lineval  48870  lincvalpr  48894  lindslinindimp2lem4  48937  zlmodzxzldeplem3  48978  zlmodzxzldeplem4  48979  itcoval0mpt  49142  ackvalsuc1mpt  49154  ackval0  49156  ackval40  49169  ackval41a  49170  ackval42  49172  ackval50  49174  ehl2eudisval0  49201  2sphere0  49226  line2  49228  line2x  49230  line2y  49231  itscnhlinecirc02p  49261  oppcup  49682  natoppf  49704