Theorem fveq1i 6879

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

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  fveq12i  6884  fvun2  6970  fvcod  6977  fvopab3ig  6982  funcnvmpt  6988  fvsnun1  7180  fvpr1g  7188  fvpr2g  7189  fvtp1  7193  fvtp2  7194  fvtp3  7195  fvtp1g  7196  fvtp2g  7197  fvtp3g  7198  fpropnf1  7264  fveqf1o  7303  ov  7557  ovigg  7558  ovg  7578  fvresex  7957  curry1  8101  curry2  8104  fsplitfpar  8115  suppsnop  8176  frrlem12  8296  fprlem1  8299  tfr2a  8384  rdgsucmptf  8417  rdgsucmptnf  8418  frsucmpt  8427  frsucmptn  8428  seqomlem1  8439  seqomlem3  8441  seqomlem4  8442  seqom0g  8445  seqomsuc  8446  unblem2  9263  inf3lemb  9604  inf3lemc  9605  ttrclselem1  9704  ttrclselem2  9705  trcl  9707  frrlem15  9739  r10  9750  r1sucg  9751  r1limg  9753  infxpenc2  10025  aleph0  10069  alephlim  10070  alephsuc  10071  alephfplem1  10107  alephfplem2  10108  ackbij2lem3  10242  cfsmolem  10272  infpssrlem1  10305  infpssrlem2  10306  fin23lem34  10348  fin23lem35  10349  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  isf34lem5  10380  hsmexlem7  10425  axdclem2  10522  canthp1lem2  10662  wunex2  10747  wuncval2  10756  addpiord  10893  mulpiord  10894  addpqnq  10947  mulpqnq  10950  fseq1p1m1  13653  om2uz0i  14011  om2uzrdg  14020  uzrdg0i  14023  uzrdgsuci  14024  hashkf  14396  hashgval  14397  hashinf  14399  ccat1st1st  14696  revs1  14834  cats1fv  14930  shftidt  15155  cbvsum  15782  cbvsumv  15783  fsumss  15811  isumclim3  15845  indsumhash  15916  isumsup2  15935  cbvprod  16002  cbvprodv  16003  fprodss  16035  iprodclim3  16087  fprodefsum  16181  ruclem4  16322  ruclem6  16323  ruclem7  16324  sadc0  16544  sadcp1  16545  sadcaddlem  16547  sadaddlem  16556  smup0  16569  smupp1  16570  algr0  16662  algrp1  16664  ndxarg  17288  strfv2d  17293  funcoppc  17964  fthepi  18019  homadm  18129  homacd  18130  prdsidlem  18876  prdsinvlem  19172  cayleylem2  19540  symggen  19597  pmtr3ncomlem1  19600  gsumval3  20034  gsumzaddlem  20048  gsumzmhm  20064  pgpfaclem1  20210  ringidval  20322  rhmsubclem2  20848  lidlval  21397  rspval  21398  lidlnegcl  21410  rspvalint  21432  lpival  21555  znf1o  21764  evlsevl  22348  selvvvval  22358  ply1ascl0  22479  ply1ascl1  22480  eqcoe1ply1eq  22524  evls1val  22545  evl1val  22554  mat1dimmul  22698  mdetralt  22830  mdetunilem7  22840  decpmatid  22995  pmatcollpwscmatlem1  23014  cpmidpmat  23098  chcoeffeq  23111  restcls  23406  restntr  23407  upxp  23849  cnmetdval  24996  remetdval  25015  qdensere2  25023  pcoptcl  25249  pcopt  25250  pcopt2  25251  pcorevlem  25254  isncvsngp  25377  cnncvsabsnegdemo  25393  ovolfsval  25698  ovollb2lem  25716  ovolunlem1a  25724  ovoliunlem1  25730  ovoliun2  25734  ovolscalem1  25741  ovolicc2lem4  25748  mblvol  25758  ioombl1lem4  25789  uniioovol  25807  uniioombllem3  25813  0pval  25899  limccnp  26118  limccnp2  26119  dvcnvrelem2  26245  itgsubstlem  26275  ply1remlem  26390  idpfv  26435  plyrem  26535  qaa  26556  abelth  26677  efif1olem4  26782  eflog  26813  logef  26818  logeftb  26820  dvrelog  26874  dvlog  26888  cxpcn3  26985  efrlim  27206  eflgam  27281  wilthlem3  27306  basellem8  27324  lgsqrlem1  27582  noetasuplem4  27972  noetainflem4  27976  precsexlem1  28472  precsexlem2  28473  precsexlem3  28474  precsexlem4  28475  precsexlem5  28476  tgcgr4  28873  krippenlem  29041  colperpexlem1  29085  opphllem3  29104  lmiisolem  29180  axlowdimlem8  29406  axlowdimlem9  29407  axlowdimlem11  29409  axlowdimlem12  29410  axlowdimlem17  29415  ushgredgedg  29689  ushgredgedgloop  29691  subgruhgredgd  29744  vtxdlfgrval  29945  vtxd0nedgb  29948  vtxdushgrfvedg  29950  vtxdginducedm1lem3  30001  finsumvtxdg2size  30010  vtxdgoddnumeven  30013  isrgr  30019  fusgrregdegfi  30029  wlk1walk  30098  wlkres  30128  wlkp1lem5  30135  wlkp1lem6  30136  wlkp1lem7  30137  wlkp1lem8  30138  clwlkcompbp  30248  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  crctcshwlkn0lem6  30283  2wlkdlem3  30395  2wlkdlem8  30401  2wlkond  30405  umgr2adedgwlk  30413  1wlkdlem4  30610  1pthond  30614  2cycld  30624  wlk2v2elem2  30636  3wlkdlem3  30641  3wlkdlem8  30647  3cycld  30658  3cyclpd  30659  eucrctshift  30723  frgrncvvdeq  30789  frgrwopreglem2  30793  ex-fpar  30942  avril1  30943  vafval  31084  smfval  31086  0vfval  31087  nmcvfval  31088  vsfval  31114  hhssabloilem  31742  pjoc2i  31919  pjcji  32165  ho0val  32231  hoival  32236  adjbdlnb  32565  nmopcoadji  32582  opsqrlem2  32622  opsqrlem5  32625  hmopidmchi  32632  hmopidmpji  32633  pjinvari  32672  pjadj2coi  32685  pj3lem1  32687  pmtrprfv2  33528  cycpmco2lem7  33572  evl1fpws  33974  mplmulmvr  34049  evlextv  34052  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  esplyindfv  34086  esplyfvn  34087  vietalem  34089  rtelextdg2lem  34236  constr0  34247  constrsuc  34248  constrlim  34249  2sqr3minply  34290  cos9thpiminplylem6  34297  madjusmdetlem1  34337  cnre2csqlem  34420  zzsnm  34469  rrhcn  34507  qqhre  34530  oms0  34808  omsmon  34809  omssubaddlem  34810  omssubadd  34811  eulerpart  34893  fib0  34910  fib1  34911  fibp1  34912  coinflippv  34995  gsumnunsn  35052  derangenlem  35750  kur14lem2  35786  kur14lem3  35787  kur14lem5  35789  kur14lem6  35790  txsconnlem  35819  cvmliftlem4  35867  cvmliftlem5  35868  satf0sucom  35952  satf0suc  35955  satf0op  35956  fmla  35960  satffunlem2lem2  35985  satfv0fvfmla0  35992  sate0  35994  funpartfv  36524  fullfunfv  36526  sumeq2si  36822  prodeq2si  36824  cbvprodvw2  36867  neibastop2lem  36979  dffinxpf  38139  ftc1cnnc  38441  heiborlem4  38564  heiborlem6  38566  cdlemk13  41725  cdlemk14  41727  cdlemk15  41728  cdlemk21N  41746  cdlemk20  41747  cdlemk56w  41846  lcfrlem1  42415  hdmapfval  42700  deg1gprod  43006  rabdiophlem2  43643  dnnumch1  43885  aomclem6  43900  mncn0  43980  aaitgo  44003  rngunsnply  44010  cytpval  44043  dssmapntrcls  44968  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  binomcxp  45181  fvmpt2df  46101  fsumsermpt  46409  fmul01  46410  fmuldfeq  46413  fmul01lt1lem1  46414  fmul01lt1lem2  46415  lptioo2cn  46473  lptioo1cn  46474  limclner  46479  dvsinax  46741  fperdvper  46747  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  dvnprodlem3  46776  itgsin0pilem1  46778  stoweidlem3  46831  stoweidlem17  46845  stoweidlem47  46875  fourierdlem42  46977  fourierdlem62  46996  fourierdlem80  47014  fourierdlem90  47024  fourierdlem92  47026  fourierdlem93  47027  fourierdlem103  47037  fourierdlem104  47038  fouriercnp  47054  sge0isum  47255  sge0seq  47274  ovnsubadd  47400  vonn0ioo  47515  vonn0icc  47516  smflimsup  47656  cjnpoly  47757  sinnpoly  47759  fcores  47955  fundcmpsurinjimaid  48311  isgrim  48798  gricushgr  48833  gpgprismgr4cycllem3  49013  gpgprismgr4cycllem6  49016  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  rhmsubcALTVlem2  49197  ply1mulgsum  49320  lineval  49324  lincvalpr  49348  lindslinindimp2lem4  49391  zlmodzxzldeplem3  49432  zlmodzxzldeplem4  49433  itcoval0mpt  49596  ackvalsuc1mpt  49608  ackval0  49610  ackval40  49623  ackval41a  49624  ackval42  49626  ackval50  49628  ehl2eudisval0  49655  2sphere0  49680  line2  49682  line2x  49684  line2y  49685  itscnhlinecirc02p  49715  oppcup  50133  natoppf  50155