Theorem fveq1i 6883

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

Syntax hints:   = wceq 1567  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  fveq12i  6888  fvun2  6974  fvcod  6981  fvopab3ig  6986  funcnvmpt  6992  fvsnun1  7181  fvpr1g  7189  fvpr2g  7190  fvtp1  7194  fvtp2  7195  fvtp3  7196  fvtp1g  7197  fvtp2g  7198  fvtp3g  7199  fpropnf1  7266  fveqf1o  7301  ov  7555  ovigg  7556  ovg  7576  fvresex  7956  curry1  8098  curry2  8101  fsplitfpar  8112  suppsnop  8173  frrlem12  8293  fprlem1  8296  tfr2a  8381  rdgsucmptf  8414  rdgsucmptnf  8415  frsucmpt  8424  frsucmptn  8425  seqomlem1  8436  seqomlem3  8438  seqomlem4  8439  seqom0g  8442  seqomsuc  8443  unblem2  9252  inf3lemb  9593  inf3lemc  9594  ttrclselem1  9693  ttrclselem2  9694  trcl  9696  frrlem15  9728  r10  9739  r1sucg  9740  r1limg  9742  infxpenc2  10005  aleph0  10049  alephlim  10050  alephsuc  10051  alephfplem1  10087  alephfplem2  10088  ackbij2lem3  10222  cfsmolem  10253  infpssrlem1  10286  infpssrlem2  10287  fin23lem34  10329  fin23lem35  10330  isf32lem6  10341  isf32lem7  10342  isf32lem8  10343  isf34lem5  10361  hsmexlem7  10406  axdclem2  10503  canthp1lem2  10637  wunex2  10722  wuncval2  10731  addpiord  10868  mulpiord  10869  addpqnq  10922  mulpqnq  10925  fseq1p1m1  13625  om2uz0i  13982  om2uzrdg  13991  uzrdg0i  13994  uzrdgsuci  13995  hashkf  14367  hashgval  14368  hashinf  14370  ccat1st1st  14665  revs1  14801  cats1fv  14895  shftidt  15118  cbvsum  15745  cbvsumv  15746  fsumss  15775  isumclim3  15809  indsumhash  15880  isumsup2  15899  cbvprod  15966  cbvprodv  15967  fprodss  16001  iprodclim3  16053  fprodefsum  16148  ruclem4  16289  ruclem6  16290  ruclem7  16291  sadc0  16511  sadcp1  16512  sadcaddlem  16514  sadaddlem  16523  smup0  16536  smupp1  16537  algr0  16629  algrp1  16631  ndxarg  17255  strfv2d  17260  funcoppc  17931  fthepi  17986  homadm  18096  homacd  18097  prdsidlem  18826  prdsinvlem  19114  cayleylem2  19482  symggen  19539  pmtr3ncomlem1  19542  gsumval3  19976  gsumzaddlem  19990  gsumzmhm  20006  pgpfaclem1  20152  ringidval  20264  rhmsubclem2  20770  lidlval  21311  rspval  21312  lidlnegcl  21324  lpival  21460  znf1o  21669  evlsevl  22251  selvvvval  22261  ply1ascl0  22382  ply1ascl1  22383  eqcoe1ply1eq  22427  evls1val  22448  evl1val  22457  mat1dimmul  22601  mdetralt  22733  mdetunilem7  22743  decpmatid  22895  pmatcollpwscmatlem1  22914  cpmidpmat  22998  chcoeffeq  23011  restcls  23306  restntr  23307  upxp  23748  cnmetdval  24895  remetdval  24914  qdensere2  24922  pcoptcl  25148  pcopt  25149  pcopt2  25150  pcorevlem  25153  isncvsngp  25276  cnncvsabsnegdemo  25292  ovolfsval  25597  ovollb2lem  25615  ovolunlem1a  25623  ovoliunlem1  25629  ovoliun2  25633  ovolscalem1  25640  ovolicc2lem4  25647  mblvol  25657  ioombl1lem4  25688  uniioovol  25706  uniioombllem3  25712  0pval  25798  limccnp  26018  limccnp2  26019  dvcnvrelem2  26145  itgsubstlem  26175  ply1remlem  26290  plyrem  26434  qaa  26452  abelth  26569  efif1olem4  26675  eflog  26706  logef  26711  logeftb  26713  dvrelog  26767  dvlog  26781  cxpcn3  26878  efrlim  27099  eflgam  27174  wilthlem3  27199  basellem8  27217  lgsqrlem1  27475  noetasuplem4  27865  noetainflem4  27869  precsexlem1  28365  precsexlem2  28366  precsexlem3  28367  precsexlem4  28368  precsexlem5  28369  tgcgr4  28765  krippenlem  28928  colperpexlem1  28969  opphllem3  28988  lmiisolem  29062  axlowdimlem8  29239  axlowdimlem9  29240  axlowdimlem11  29242  axlowdimlem12  29243  axlowdimlem17  29248  ushgredgedg  29519  ushgredgedgloop  29521  subgruhgredgd  29574  vtxdlfgrval  29775  vtxd0nedgb  29778  vtxdushgrfvedg  29780  vtxdginducedm1lem3  29831  finsumvtxdg2size  29840  vtxdgoddnumeven  29843  isrgr  29849  fusgrregdegfi  29859  wlk1walk  29928  wlkres  29958  wlkp1lem5  29965  wlkp1lem6  29966  wlkp1lem7  29967  wlkp1lem8  29968  clwlkcompbp  30071  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  2wlkdlem3  30216  2wlkdlem8  30222  2wlkond  30226  umgr2adedgwlk  30234  1wlkdlem4  30431  1pthond  30435  wlk2v2elem2  30447  3wlkdlem3  30452  3wlkdlem8  30458  3cycld  30469  3cyclpd  30470  eucrctshift  30534  frgrncvvdeq  30600  frgrwopreglem2  30604  ex-fpar  30753  avril1  30754  vafval  30895  smfval  30897  0vfval  30898  nmcvfval  30899  vsfval  30925  hhssabloilem  31553  pjoc2i  31730  pjcji  31976  ho0val  32042  hoival  32047  adjbdlnb  32376  nmopcoadji  32393  opsqrlem2  32433  opsqrlem5  32436  hmopidmchi  32443  hmopidmpji  32444  pjinvari  32483  pjadj2coi  32496  pj3lem1  32498  pmtrprfv2  33348  cycpmco2lem7  33392  evl1fpws  33798  mplmulmvr  33873  evlextv  33876  esplyfval1  33907  esplyfvaln  33908  esplyind  33909  esplyindfv  33910  esplyfvn  33911  vietalem  33913  rtelextdg2lem  34060  constr0  34071  constrsuc  34072  constrlim  34073  2sqr3minply  34114  cos9thpiminplylem6  34121  madjusmdetlem1  34161  cnre2csqlem  34244  zzsnm  34293  rrhcn  34331  qqhre  34354  oms0  34631  omsmon  34632  omssubaddlem  34633  omssubadd  34634  eulerpart  34716  fib0  34733  fib1  34734  fibp1  34735  coinflippv  34818  gsumnunsn  34875  2cycld  35528  derangenlem  35561  kur14lem2  35597  kur14lem3  35598  kur14lem5  35600  kur14lem6  35601  txsconnlem  35630  cvmliftlem4  35678  cvmliftlem5  35679  satf0sucom  35763  satf0suc  35766  satf0op  35767  fmla  35771  satffunlem2lem2  35796  satfv0fvfmla0  35803  sate0  35805  funpartfv  36335  fullfunfv  36337  sumeq2si  36602  prodeq2si  36604  cbvprodvw2  36647  neibastop2lem  36759  dffinxpf  37918  ftc1cnnc  38230  heiborlem4  38352  heiborlem6  38354  cdlemk13  41515  cdlemk14  41517  cdlemk15  41518  cdlemk21N  41536  cdlemk20  41537  cdlemk56w  41636  lcfrlem1  42205  hdmapfval  42490  deg1gprod  42796  rabdiophlem2  43420  dnnumch1  43662  aomclem6  43677  mncn0  43757  aaitgo  43780  rngunsnply  43787  cytpval  43820  dssmapntrcls  44745  binomcxplemdvsum  44956  binomcxplemnotnn0  44957  binomcxp  44958  fvmpt2df  45878  fsumsermpt  46186  fmul01  46187  fmuldfeq  46190  fmul01lt1lem1  46191  fmul01lt1lem2  46192  lptioo2cn  46250  lptioo1cn  46251  limclner  46256  dvsinax  46518  fperdvper  46524  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  dvnprodlem3  46553  itgsin0pilem1  46555  stoweidlem3  46608  stoweidlem17  46622  stoweidlem47  46652  fourierdlem42  46754  fourierdlem62  46773  fourierdlem80  46791  fourierdlem90  46801  fourierdlem92  46803  fourierdlem93  46804  fourierdlem103  46814  fourierdlem104  46815  fouriercnp  46831  sge0isum  47032  sge0seq  47051  ovnsubadd  47177  vonn0ioo  47292  vonn0icc  47293  smflimsup  47433  cjnpoly  47514  sinnpoly  47516  fcores  47692  fundcmpsurinjimaid  48048  isgrim  48535  gricushgr  48570  gpgprismgr4cycllem3  48750  gpgprismgr4cycllem6  48753  gpgprismgr4cycllem7  48754  gpgprismgr4cycllem10  48757  rhmsubcALTVlem2  48935  ply1mulgsum  49054  lineval  49058  lincvalpr  49082  lindslinindimp2lem4  49125  zlmodzxzldeplem3  49166  zlmodzxzldeplem4  49167  itcoval0mpt  49330  ackvalsuc1mpt  49342  ackval0  49344  ackval40  49357  ackval41a  49358  ackval42  49360  ackval50  49362  ehl2eudisval0  49389  2sphere0  49414  line2  49416  line2x  49418  line2y  49419  itscnhlinecirc02p  49449  oppcup  49869  natoppf  49891