Theorem fveq1i 6882

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

Syntax hints:   = wceq 1570  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is referenced by:  fveq12i  6887  fvun2  6973  fvcod  6980  fvopab3ig  6985  funcnvmpt  6991  fvsnun1  7180  fvpr1g  7188  fvpr2g  7189  fvtp1  7193  fvtp2  7194  fvtp3  7195  fvtp1g  7196  fvtp2g  7197  fvtp3g  7198  fpropnf1  7265  fveqf1o  7300  ov  7554  ovigg  7555  ovg  7575  fvresex  7953  curry1  8095  curry2  8098  fsplitfpar  8109  suppsnop  8170  frrlem12  8290  fprlem1  8293  tfr2a  8378  rdgsucmptf  8411  rdgsucmptnf  8412  frsucmpt  8421  frsucmptn  8422  seqomlem1  8433  seqomlem3  8435  seqomlem4  8436  seqom0g  8439  seqomsuc  8440  unblem2  9249  inf3lemb  9590  inf3lemc  9591  ttrclselem1  9690  ttrclselem2  9691  trcl  9693  frrlem15  9725  r10  9736  r1sucg  9737  r1limg  9739  infxpenc2  10002  aleph0  10046  alephlim  10047  alephsuc  10048  alephfplem1  10084  alephfplem2  10085  ackbij2lem3  10219  cfsmolem  10249  infpssrlem1  10282  infpssrlem2  10283  fin23lem34  10325  fin23lem35  10326  isf32lem6  10337  isf32lem7  10338  isf32lem8  10339  isf34lem5  10357  hsmexlem7  10402  axdclem2  10499  canthp1lem2  10633  wunex2  10718  wuncval2  10727  addpiord  10864  mulpiord  10865  addpqnq  10918  mulpqnq  10921  fseq1p1m1  13622  om2uz0i  13979  om2uzrdg  13988  uzrdg0i  13991  uzrdgsuci  13992  hashkf  14364  hashgval  14365  hashinf  14367  ccat1st1st  14662  revs1  14798  cats1fv  14892  shftidt  15115  cbvsum  15742  cbvsumv  15743  fsumss  15772  isumclim3  15806  indsumhash  15877  isumsup2  15896  cbvprod  15963  cbvprodv  15964  fprodss  15998  iprodclim3  16050  fprodefsum  16144  ruclem4  16285  ruclem6  16286  ruclem7  16287  sadc0  16507  sadcp1  16508  sadcaddlem  16510  sadaddlem  16519  smup0  16532  smupp1  16533  algr0  16625  algrp1  16627  ndxarg  17251  strfv2d  17256  funcoppc  17927  fthepi  17982  homadm  18092  homacd  18093  prdsidlem  18822  prdsinvlem  19110  cayleylem2  19478  symggen  19535  pmtr3ncomlem1  19538  gsumval3  19972  gsumzaddlem  19986  gsumzmhm  20002  pgpfaclem1  20148  ringidval  20260  rhmsubclem2  20785  lidlval  21334  rspval  21335  lidlnegcl  21347  rspvalint  21369  lpival  21492  znf1o  21701  evlsevl  22283  selvvvval  22293  ply1ascl0  22414  ply1ascl1  22415  eqcoe1ply1eq  22459  evls1val  22480  evl1val  22489  mat1dimmul  22633  mdetralt  22765  mdetunilem7  22775  decpmatid  22927  pmatcollpwscmatlem1  22946  cpmidpmat  23030  chcoeffeq  23043  restcls  23338  restntr  23339  upxp  23780  cnmetdval  24927  remetdval  24946  qdensere2  24954  pcoptcl  25180  pcopt  25181  pcopt2  25182  pcorevlem  25185  isncvsngp  25308  cnncvsabsnegdemo  25324  ovolfsval  25629  ovollb2lem  25647  ovolunlem1a  25655  ovoliunlem1  25661  ovoliun2  25665  ovolscalem1  25672  ovolicc2lem4  25679  mblvol  25689  ioombl1lem4  25720  uniioovol  25738  uniioombllem3  25744  0pval  25830  limccnp  26050  limccnp2  26051  dvcnvrelem2  26177  itgsubstlem  26207  ply1remlem  26322  plyrem  26466  qaa  26484  abelth  26604  efif1olem4  26710  eflog  26741  logef  26746  logeftb  26748  dvrelog  26802  dvlog  26816  cxpcn3  26913  efrlim  27134  eflgam  27209  wilthlem3  27234  basellem8  27252  lgsqrlem1  27510  noetasuplem4  27900  noetainflem4  27904  precsexlem1  28400  precsexlem2  28401  precsexlem3  28402  precsexlem4  28403  precsexlem5  28404  tgcgr4  28800  krippenlem  28967  colperpexlem1  29011  opphllem3  29030  lmiisolem  29105  axlowdimlem8  29299  axlowdimlem9  29300  axlowdimlem11  29302  axlowdimlem12  29303  axlowdimlem17  29308  ushgredgedg  29579  ushgredgedgloop  29581  subgruhgredgd  29634  vtxdlfgrval  29835  vtxd0nedgb  29838  vtxdushgrfvedg  29840  vtxdginducedm1lem3  29891  finsumvtxdg2size  29900  vtxdgoddnumeven  29903  isrgr  29909  fusgrregdegfi  29919  wlk1walk  29988  wlkres  30018  wlkp1lem5  30025  wlkp1lem6  30026  wlkp1lem7  30027  wlkp1lem8  30028  clwlkcompbp  30131  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  2wlkdlem3  30276  2wlkdlem8  30282  2wlkond  30286  umgr2adedgwlk  30294  1wlkdlem4  30491  1pthond  30495  wlk2v2elem2  30507  3wlkdlem3  30512  3wlkdlem8  30518  3cycld  30529  3cyclpd  30530  eucrctshift  30594  frgrncvvdeq  30660  frgrwopreglem2  30664  ex-fpar  30813  avril1  30814  vafval  30955  smfval  30957  0vfval  30958  nmcvfval  30959  vsfval  30985  hhssabloilem  31613  pjoc2i  31790  pjcji  32036  ho0val  32102  hoival  32107  adjbdlnb  32436  nmopcoadji  32453  opsqrlem2  32493  opsqrlem5  32496  hmopidmchi  32503  hmopidmpji  32504  pjinvari  32543  pjadj2coi  32556  pj3lem1  32558  pmtrprfv2  33408  cycpmco2lem7  33452  evl1fpws  33854  mplmulmvr  33929  evlextv  33932  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vietalem  33969  rtelextdg2lem  34116  constr0  34127  constrsuc  34128  constrlim  34129  2sqr3minply  34170  cos9thpiminplylem6  34177  madjusmdetlem1  34217  cnre2csqlem  34300  zzsnm  34349  rrhcn  34387  qqhre  34410  oms0  34687  omsmon  34688  omssubaddlem  34689  omssubadd  34690  eulerpart  34772  fib0  34789  fib1  34790  fibp1  34791  coinflippv  34874  gsumnunsn  34931  2cycld  35630  derangenlem  35663  kur14lem2  35699  kur14lem3  35700  kur14lem5  35702  kur14lem6  35703  txsconnlem  35732  cvmliftlem4  35780  cvmliftlem5  35781  satf0sucom  35865  satf0suc  35868  satf0op  35869  fmla  35873  satffunlem2lem2  35898  satfv0fvfmla0  35905  sate0  35907  funpartfv  36437  fullfunfv  36439  sumeq2si  36714  prodeq2si  36716  cbvprodvw2  36759  neibastop2lem  36871  dffinxpf  38031  ftc1cnnc  38343  heiborlem4  38465  heiborlem6  38467  cdlemk13  41626  cdlemk14  41628  cdlemk15  41629  cdlemk21N  41647  cdlemk20  41648  cdlemk56w  41747  lcfrlem1  42316  hdmapfval  42601  deg1gprod  42907  rabdiophlem2  43529  dnnumch1  43771  aomclem6  43786  mncn0  43866  aaitgo  43889  rngunsnply  43896  cytpval  43929  dssmapntrcls  44854  binomcxplemdvsum  45065  binomcxplemnotnn0  45066  binomcxp  45067  fvmpt2df  45987  fsumsermpt  46295  fmul01  46296  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  lptioo2cn  46359  lptioo1cn  46360  limclner  46365  dvsinax  46627  fperdvper  46633  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  itgsin0pilem1  46664  stoweidlem3  46717  stoweidlem17  46731  stoweidlem47  46761  fourierdlem42  46863  fourierdlem62  46882  fourierdlem80  46900  fourierdlem90  46910  fourierdlem92  46912  fourierdlem93  46913  fourierdlem103  46923  fourierdlem104  46924  fouriercnp  46940  sge0isum  47141  sge0seq  47160  ovnsubadd  47286  vonn0ioo  47401  vonn0icc  47402  smflimsup  47542  cjnpoly  47626  sinnpoly  47628  fcores  47804  fundcmpsurinjimaid  48160  isgrim  48647  gricushgr  48682  gpgprismgr4cycllem3  48862  gpgprismgr4cycllem6  48865  gpgprismgr4cycllem7  48866  gpgprismgr4cycllem10  48869  rhmsubcALTVlem2  49047  ply1mulgsum  49170  lineval  49174  lincvalpr  49198  lindslinindimp2lem4  49241  zlmodzxzldeplem3  49282  zlmodzxzldeplem4  49283  itcoval0mpt  49446  ackvalsuc1mpt  49458  ackval0  49460  ackval40  49473  ackval41a  49474  ackval42  49476  ackval50  49478  ehl2eudisval0  49505  2sphere0  49530  line2  49532  line2x  49534  line2y  49535  itscnhlinecirc02p  49565  oppcup  49985  natoppf  50007