Theorem fveq1i 6889

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

This proof depends on syntax axioms:   = wceq 1569  ‘cfv 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549

This theorem is used by:  fveq12i  6894  fvun2  6980  fvcod  6987  fvopab3ig  6992  funcnvmpt  6998  fvsnun1  7189  fvpr1g  7197  fvpr2g  7198  fvtp1  7202  fvtp2  7203  fvtp3  7204  fvtp1g  7205  fvtp2g  7206  fvtp3g  7207  fpropnf1  7273  fveqf1o  7312  ov  7566  ovigg  7567  ovg  7587  mpt3fvd  7690  fvresex  7974  curry1  8119  curry2  8122  fsplitfpar  8133  suppsnop  8200  frrlem12  8320  fprlem1  8323  tfr2a  8408  rdgsucmptf  8441  rdgsucmptnf  8442  frsucmpt  8451  frsucmptn  8452  seqomlem1  8465  seqomlem3  8467  seqomlem4  8468  seqom0g  8471  seqomsuc  8472  unblem2  9290  inf3lemb  9631  inf3lemc  9632  ttrclselem1  9731  ttrclselem2  9732  trcl  9734  frrlem15  9766  r10  9780  r1sucg  9781  r1limg  9783  infxpenc2  10106  aleph0  10150  alephlim  10151  alephsuc  10152  alephfplem1  10188  alephfplem2  10189  ackbij2lem3  10323  cfsmolem  10353  infpssrlem1  10386  infpssrlem2  10387  fin23lem34  10429  fin23lem35  10430  isf32lem6  10441  isf32lem7  10442  isf32lem8  10443  isf34lem5  10461  hsmexlem7  10506  axdclem2  10603  canthp1lem2  10743  wunex2  10828  wuncval2  10837  addpiord  10974  mulpiord  10975  addpqnq  11028  mulpqnq  11031  fseq1p1m1  13737  om2uz0i  14095  om2uzrdg  14104  uzrdg0i  14107  uzrdgsuci  14108  hashkf  14481  hashgval  14482  hashinf  14484  ccat1st1st  14782  revs1  14920  cats1fv  15016  shftidt  15242  cbvsum  15869  cbvsumv  15870  fsumss  15898  isumclim3  15932  indsumhash  16003  isumsup2  16022  cbvprod  16089  cbvprodv  16090  fprodss  16122  iprodclim3  16174  fprodefsum  16268  ruclem4  16409  ruclem6  16410  ruclem7  16411  sadc0  16631  sadcp1  16632  sadcaddlem  16634  sadaddlem  16643  smup0  16656  smupp1  16657  algr0  16754  algrp1  16756  ndxarg  17381  strfv2d  17386  funcoppc  18057  fthepi  18112  homadm  18222  homacd  18223  prdsidlem  18970  prdsinvlem  19266  cayleylem2  19634  symggen  19691  pmtr3ncomlem1  19694  gsumval3  20128  gsumzaddlem  20142  gsumzmhm  20158  pgpfaclem1  20304  ringidval  20416  rhmsubclem2  20945  lidlval  21495  rspval  21496  lidlnegcl  21508  rspvalint  21530  lpival  21655  znf1o  21864  evlsevl  22448  selvvvval  22458  ply1ascl0  22579  ply1ascl1  22580  eqcoe1ply1eq  22624  evls1val  22645  evl1val  22654  mat1dimmul  22798  mdetralt  22930  mdetunilem7  22940  decpmatid  23095  pmatcollpwscmatlem1  23114  cpmidpmat  23198  chcoeffeq  23211  restcls  23506  restntr  23507  upxp  23949  cnmetdval  25096  remetdval  25115  qdensere2  25123  pcoptcl  25349  pcopt  25350  pcopt2  25351  pcorevlem  25354  isncvsngp  25477  cnncvsabsnegdemo  25493  ovolfsval  25798  ovollb2lem  25816  ovolunlem1a  25824  ovoliunlem1  25830  ovoliun2  25834  ovolscalem1  25841  ovolicc2lem4  25848  mblvol  25858  ioombl1lem4  25889  uniioovol  25907  uniioombllem3  25913  0pval  25999  limccnp  26218  limccnp2  26219  dvcnvrelem2  26345  itgsubstlem  26375  ply1remlem  26490  idpfv  26535  plyrem  26633  abelth  26775  efif1olem4  26880  eflog  26911  logef  26916  logeftb  26918  dvrelog  26972  dvlog  26986  cxpcn3  27083  efrlim  27304  eflgam  27379  wilthlem3  27404  basellem8  27422  lgsqrlem1  27680  noetasuplem4  28100  noetainflem4  28104  precsexlem1  28600  precsexlem2  28601  precsexlem3  28602  precsexlem4  28603  precsexlem5  28604  tgcgr4  29001  krippenlem  29169  colperpexlem1  29213  opphllem3  29232  lmiisolem  29308  axlowdimlem8  29534  axlowdimlem9  29535  axlowdimlem11  29537  axlowdimlem12  29538  axlowdimlem17  29543  ushgredgedg  29817  ushgredgedgloop  29819  subgruhgredgd  29872  vtxdlfgrval  30073  vtxd0nedgb  30076  vtxdushgrfvedg  30078  vtxdginducedm1lem3  30129  finsumvtxdg2size  30138  vtxdgoddnumeven  30141  isrgr  30147  fusgrregdegfi  30157  wlk1walk  30226  wlkres  30256  wlkp1lem5  30263  wlkp1lem6  30264  wlkp1lem7  30265  wlkp1lem8  30266  clwlkcompbp  30376  crctcshwlkn0lem4  30409  crctcshwlkn0lem5  30410  crctcshwlkn0lem6  30411  2wlkdlem3  30523  2wlkdlem8  30529  2wlkond  30533  umgr2adedgwlk  30541  1wlkdlem4  30738  1pthond  30742  2cycld  30752  wlk2v2elem2  30764  3wlkdlem3  30769  3wlkdlem8  30775  3cycld  30786  3cyclpd  30787  eucrctshift  30851  frgrncvvdeq  30917  frgrwopreglem2  30921  ex-fpar  31070  avril1  31071  vafval  31212  smfval  31214  0vfval  31215  nmcvfval  31216  vsfval  31242  hhssabloilem  31870  pjoc2i  32047  pjcji  32293  ho0val  32359  hoival  32364  adjbdlnb  32693  nmopcoadji  32710  opsqrlem2  32750  opsqrlem5  32753  hmopidmchi  32760  hmopidmpji  32761  pjinvari  32800  pjadj2coi  32813  pj3lem1  32815  pmtrprfv2  33697  cycpmco2lem7  33741  evl1fpws  34144  mplmulmvr  34219  evlextv  34222  esplyfval1  34253  esplyfvaln  34254  esplyind  34255  esplyindfv  34256  esplyfvn  34257  vietalem  34259  rtelextdg2lem  34406  constr0  34417  constrsuc  34418  constrlim  34419  2sqr3minply  34460  cos9thpiminplylem6  34467  madjusmdetlem1  34507  cnre2csqlem  34590  zzsnm  34639  rrhcn  34677  qqhre  34700  oms0  34977  omsmon  34978  omssubaddlem  34979  omssubadd  34980  eulerpart  35062  fib0  35079  fib1  35080  fibp1  35081  coinflippv  35164  gsumnunsn  35221  fwfffunres  35766  derangenlem  36024  kur14lem2  36060  kur14lem3  36061  kur14lem5  36063  kur14lem6  36064  txsconnlem  36093  cvmliftlem4  36141  cvmliftlem5  36142  satf0sucom  36226  satf0suc  36229  satf0op  36230  fmla  36234  satffunlem2lem2  36259  satfv0fvfmla0  36266  sate0  36268  funpartfv  36803  fullfunfv  36805  sumeq2si  37085  prodeq2si  37087  cbvprodvw2  37130  neibastop2lem  37242  dffinxpf  38415  ftc1cnnc  38717  heiborlem4  38855  heiborlem6  38857  cdlemk13  42016  cdlemk14  42018  cdlemk15  42019  cdlemk21N  42037  cdlemk20  42038  cdlemk56w  42137  lcfrlem1  42706  hdmapfval  42991  deg1gprod  43297  rabdiophlem2  43916  dnnumch1  44158  aomclem6  44168  mncn0  44248  aaitgo  44271  rngunsnply  44278  cytpval  44311  dssmapntrcls  45235  binomcxplemdvsum  45446  binomcxplemnotnn0  45447  binomcxp  45448  fvmpt2df  46391  fsumsermpt  46698  fmul01  46699  fmuldfeq  46702  fmul01lt1lem1  46703  fmul01lt1lem2  46704  lptioo2cn  46762  lptioo1cn  46763  limclner  46768  dvsinax  47030  fperdvper  47036  dvnmul  47060  dvnprodlem1  47063  dvnprodlem2  47064  dvnprodlem3  47065  itgsin0pilem1  47067  stoweidlem3  47120  stoweidlem17  47134  stoweidlem47  47164  fourierdlem42  47266  fourierdlem62  47285  fourierdlem80  47303  fourierdlem90  47313  fourierdlem92  47315  fourierdlem93  47316  fourierdlem103  47326  fourierdlem104  47327  fouriercnp  47343  sge0isum  47544  sge0seq  47563  ovnsubadd  47689  vonn0ioo  47804  vonn0icc  47805  smflimsup  47945  cjnpoly  48046  sinnpoly  48048  fcores  48244  fundcmpsurinjimaid  48600  isgrim  49087  gricushgr  49122  gpgprismgr4cycllem3  49302  gpgprismgr4cycllem6  49305  gpgprismgr4cycllem7  49306  gpgprismgr4cycllem10  49309  rhmsubcALTVlem2  49486  ply1mulgsum  49609  lineval  49613  lincvalpr  49637  lindslinindimp2lem4  49680  zlmodzxzldeplem3  49721  zlmodzxzldeplem4  49722  itcoval0mpt  49885  ackvalsuc1mpt  49897  ackval0  49899  ackval40  49912  ackval41a  49913  ackval42  49915  ackval50  49917  ehl2eudisval0  49945  2sphere0  49969  line2  49971  line2x  49973  line2y  49974  oppcup  50430  natoppf  50458  par2diag  50887  fuconuniqvalslem  50890