Theorem fveq1i 6835

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

Syntax hints:   = wceq 1541  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  fveq12i  6840  fvun2  6926  fvopab3ig  6937  fvsnun1  7128  fvpr1g  7136  fvpr2g  7137  fvtp1  7141  fvtp2  7142  fvtp3  7143  fvtp1g  7144  fvtp2g  7145  fvtp3g  7146  fpropnf1  7213  fveqf1o  7248  ov  7502  ovigg  7503  ovg  7523  fvresex  7904  curry1  8046  curry2  8049  fsplitfpar  8060  suppsnop  8120  frrlem12  8239  fprlem1  8242  tfr2a  8326  rdgsucmptf  8359  rdgsucmptnf  8360  frsucmpt  8369  frsucmptn  8370  seqomlem1  8381  seqomlem3  8383  seqomlem4  8384  seqom0g  8387  seqomsuc  8388  unblem2  9193  inf3lemb  9534  inf3lemc  9535  ttrclselem1  9634  ttrclselem2  9635  trcl  9637  frrlem15  9669  r10  9680  r1sucg  9681  r1limg  9683  infxpenc2  9932  aleph0  9976  alephlim  9977  alephsuc  9978  alephfplem1  10014  alephfplem2  10015  ackbij2lem3  10150  cfsmolem  10180  infpssrlem1  10213  infpssrlem2  10214  fin23lem34  10256  fin23lem35  10257  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  isf34lem5  10288  hsmexlem7  10333  axdclem2  10430  canthp1lem2  10564  wunex2  10649  wuncval2  10658  addpiord  10795  mulpiord  10796  addpqnq  10849  mulpqnq  10852  fseq1p1m1  13514  om2uz0i  13870  om2uzrdg  13879  uzrdg0i  13882  uzrdgsuci  13883  hashkf  14255  hashgval  14256  hashinf  14258  ccat1st1st  14552  revs1  14688  cats1fv  14782  shftidt  15005  cbvsum  15618  cbvsumv  15619  fsumss  15648  isumclim3  15682  isumsup2  15769  cbvprod  15836  cbvprodv  15837  fprodss  15871  iprodclim3  15923  fprodefsum  16018  ruclem4  16159  ruclem6  16160  ruclem7  16161  sadc0  16381  sadcp1  16382  sadcaddlem  16384  sadaddlem  16393  smup0  16406  smupp1  16407  algr0  16499  algrp1  16501  ndxarg  17123  strfv2d  17128  funcoppc  17799  fthepi  17854  homadm  17964  homacd  17965  prdsidlem  18694  prdsinvlem  18979  cayleylem2  19342  symggen  19399  pmtr3ncomlem1  19402  gsumval3  19836  gsumzaddlem  19850  gsumzmhm  19866  pgpfaclem1  20012  ringidval  20118  rhmsubclem2  20619  lidlval  21165  rspval  21166  lidlnegcl  21177  lpival  21279  znf1o  21506  ply1ascl0  22195  ply1ascl1  22196  eqcoe1ply1eq  22243  evls1val  22264  evl1val  22273  mat1dimmul  22420  mdetralt  22552  mdetunilem7  22562  decpmatid  22714  pmatcollpwscmatlem1  22733  cpmidpmat  22817  chcoeffeq  22830  restcls  23125  restntr  23126  upxp  23567  cnmetdval  24714  remetdval  24733  qdensere2  24741  pcoptcl  24977  pcopt  24978  pcopt2  24979  pcorevlem  24982  isncvsngp  25105  cnncvsabsnegdemo  25121  ovolfsval  25427  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliun2  25463  ovolscalem1  25470  ovolicc2lem4  25477  mblvol  25487  ioombl1lem4  25518  uniioovol  25536  uniioombllem3  25542  0pval  25628  limccnp  25848  limccnp2  25849  dvcnvrelem2  25979  itgsubstlem  26011  ply1remlem  26126  plyrem  26269  qaa  26287  abelth  26407  efif1olem4  26510  eflog  26541  logef  26546  logeftb  26548  dvrelog  26602  dvlog  26616  cxpcn3  26714  efrlim  26935  efrlimOLD  26936  eflgam  27011  wilthlem3  27036  basellem8  27054  lgsqrlem1  27313  noetasuplem4  27704  noetainflem4  27708  precsexlem1  28203  precsexlem2  28204  precsexlem3  28205  precsexlem4  28206  precsexlem5  28207  tgcgr4  28603  krippenlem  28762  colperpexlem1  28802  opphllem3  28821  lmiisolem  28868  axlowdimlem8  29022  axlowdimlem9  29023  axlowdimlem11  29025  axlowdimlem12  29026  axlowdimlem17  29031  ushgredgedg  29302  ushgredgedgloop  29304  subgruhgredgd  29357  vtxdlfgrval  29559  vtxd0nedgb  29562  vtxdushgrfvedg  29564  vtxdginducedm1lem3  29615  finsumvtxdg2size  29624  vtxdgoddnumeven  29627  isrgr  29633  fusgrregdegfi  29643  wlk1walk  29712  wlkres  29742  wlkp1lem5  29749  wlkp1lem6  29750  wlkp1lem7  29751  wlkp1lem8  29752  clwlkcompbp  29855  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  2wlkdlem3  30000  2wlkdlem8  30006  2wlkond  30010  umgr2adedgwlk  30018  1wlkdlem4  30215  1pthond  30219  wlk2v2elem2  30231  3wlkdlem3  30236  3wlkdlem8  30242  3cycld  30253  3cyclpd  30254  eucrctshift  30318  frgrncvvdeq  30384  frgrwopreglem2  30388  ex-fpar  30537  avril1  30538  vafval  30678  smfval  30680  0vfval  30681  nmcvfval  30682  vsfval  30708  hhssabloilem  31336  pjoc2i  31513  pjcji  31759  ho0val  31825  hoival  31830  adjbdlnb  32159  nmopcoadji  32176  opsqrlem2  32216  opsqrlem5  32219  hmopidmchi  32226  hmopidmpji  32227  pjinvari  32266  pjadj2coi  32279  pj3lem1  32281  funcnvmpt  32745  pmtrprfv2  33170  cycpmco2lem7  33214  evl1fpws  33645  mplmulmvr  33704  evlextv  33707  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vietalem  33735  rgmoddimOLD  33767  rtelextdg2lem  33883  constr0  33894  constrsuc  33895  constrlim  33896  2sqr3minply  33937  cos9thpiminplylem6  33944  madjusmdetlem1  33984  cnre2csqlem  34067  zzsnm  34116  rrhcn  34154  qqhre  34177  oms0  34454  omsmon  34455  omssubaddlem  34456  omssubadd  34457  eulerpart  34539  fib0  34556  fib1  34557  fibp1  34558  coinflippv  34641  gsumnunsn  34698  2cycld  35332  derangenlem  35365  kur14lem2  35401  kur14lem3  35402  kur14lem5  35404  kur14lem6  35405  txsconnlem  35434  cvmliftlem4  35482  cvmliftlem5  35483  satf0sucom  35567  satf0suc  35570  satf0op  35571  fmla  35575  satffunlem2lem2  35600  satfv0fvfmla0  35607  sate0  35609  funpartfv  36139  fullfunfv  36141  sumeq2si  36396  prodeq2si  36398  cbvprodvw2  36441  neibastop2lem  36554  dffinxpf  37590  ftc1cnnc  37893  heiborlem4  38015  heiborlem6  38017  cdlemk13  41112  cdlemk14  41114  cdlemk15  41115  cdlemk21N  41133  cdlemk20  41134  cdlemk56w  41233  lcfrlem1  41802  hdmapfval  42087  deg1gprod  42394  evlsevl  42817  selvvvval  42828  rabdiophlem2  43044  dnnumch1  43286  aomclem6  43301  mncn0  43381  aaitgo  43404  rngunsnply  43411  cytpval  43444  dssmapntrcls  44369  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  binomcxp  44598  fvcod  45471  fvmpt2df  45516  fsumsermpt  45825  fmul01  45826  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  lptioo2cn  45889  lptioo1cn  45890  limclner  45895  dvsinax  46157  fperdvper  46163  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  itgsin0pilem1  46194  stoweidlem3  46247  stoweidlem17  46261  stoweidlem47  46291  fourierdlem42  46393  fourierdlem62  46412  fourierdlem80  46430  fourierdlem90  46440  fourierdlem92  46442  fourierdlem93  46443  fourierdlem103  46453  fourierdlem104  46454  fouriercnp  46470  sge0isum  46671  sge0seq  46690  ovnsubadd  46816  vonn0ioo  46931  vonn0icc  46932  smflimsup  47072  cjnpoly  47135  sinnpoly  47137  fcores  47313  fundcmpsurinjimaid  47657  isgrim  48128  gricushgr  48163  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem6  48346  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem10  48350  rhmsubcALTVlem2  48528  ply1mulgsum  48636  lineval  48640  lincvalpr  48664  lindslinindimp2lem4  48707  zlmodzxzldeplem3  48748  zlmodzxzldeplem4  48749  itcoval0mpt  48912  ackvalsuc1mpt  48924  ackval0  48926  ackval40  48939  ackval41a  48940  ackval42  48942  ackval50  48944  ehl2eudisval0  48971  2sphere0  48996  line2  48998  line2x  49000  line2y  49001  itscnhlinecirc02p  49031  oppcup  49452  natoppf  49474