Theorem fveq1i 6886

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  fveq12i  6891  fvun2  6977  fvcod  6984  fvopab3ig  6989  funcnvmpt  6995  fvsnun1  7186  fvpr1g  7194  fvpr2g  7195  fvtp1  7199  fvtp2  7200  fvtp3  7201  fvtp1g  7202  fvtp2g  7203  fvtp3g  7204  fpropnf1  7270  fveqf1o  7309  ov  7563  ovigg  7564  ovg  7584  fvresex  7963  curry1  8105  curry2  8108  fsplitfpar  8119  suppsnop  8180  frrlem12  8300  fprlem1  8303  tfr2a  8388  rdgsucmptf  8421  rdgsucmptnf  8422  frsucmpt  8431  frsucmptn  8432  seqomlem1  8443  seqomlem3  8445  seqomlem4  8446  seqom0g  8449  seqomsuc  8450  unblem2  9260  inf3lemb  9601  inf3lemc  9602  ttrclselem1  9701  ttrclselem2  9702  trcl  9704  frrlem15  9736  r10  9747  r1sucg  9748  r1limg  9750  infxpenc2  10022  aleph0  10066  alephlim  10067  alephsuc  10068  alephfplem1  10104  alephfplem2  10105  ackbij2lem3  10239  cfsmolem  10269  infpssrlem1  10302  infpssrlem2  10303  fin23lem34  10345  fin23lem35  10346  isf32lem6  10357  isf32lem7  10358  isf32lem8  10359  isf34lem5  10377  hsmexlem7  10422  axdclem2  10519  canthp1lem2  10653  wunex2  10738  wuncval2  10747  addpiord  10884  mulpiord  10885  addpqnq  10938  mulpqnq  10941  fseq1p1m1  13643  om2uz0i  14001  om2uzrdg  14010  uzrdg0i  14013  uzrdgsuci  14014  hashkf  14386  hashgval  14387  hashinf  14389  ccat1st1st  14686  revs1  14824  cats1fv  14920  shftidt  15143  cbvsum  15770  cbvsumv  15771  fsumss  15799  isumclim3  15833  indsumhash  15904  isumsup2  15923  cbvprod  15990  cbvprodv  15991  fprodss  16025  iprodclim3  16077  fprodefsum  16171  ruclem4  16312  ruclem6  16313  ruclem7  16314  sadc0  16534  sadcp1  16535  sadcaddlem  16537  sadaddlem  16546  smup0  16559  smupp1  16560  algr0  16652  algrp1  16654  ndxarg  17278  strfv2d  17283  funcoppc  17954  fthepi  18009  homadm  18119  homacd  18120  prdsidlem  18864  prdsinvlem  19159  cayleylem2  19527  symggen  19584  pmtr3ncomlem1  19587  gsumval3  20021  gsumzaddlem  20035  gsumzmhm  20051  pgpfaclem1  20197  ringidval  20309  rhmsubclem2  20835  lidlval  21384  rspval  21385  lidlnegcl  21397  rspvalint  21419  lpival  21542  znf1o  21751  evlsevl  22333  selvvvval  22343  ply1ascl0  22464  ply1ascl1  22465  eqcoe1ply1eq  22509  evls1val  22530  evl1val  22539  mat1dimmul  22683  mdetralt  22815  mdetunilem7  22825  decpmatid  22977  pmatcollpwscmatlem1  22996  cpmidpmat  23080  chcoeffeq  23093  restcls  23388  restntr  23389  upxp  23831  cnmetdval  24978  remetdval  24997  qdensere2  25005  pcoptcl  25231  pcopt  25232  pcopt2  25233  pcorevlem  25236  isncvsngp  25359  cnncvsabsnegdemo  25375  ovolfsval  25680  ovollb2lem  25698  ovolunlem1a  25706  ovoliunlem1  25712  ovoliun2  25716  ovolscalem1  25723  ovolicc2lem4  25730  mblvol  25740  ioombl1lem4  25771  uniioovol  25789  uniioombllem3  25795  0pval  25881  limccnp  26101  limccnp2  26102  dvcnvrelem2  26228  itgsubstlem  26258  ply1remlem  26373  plyrem  26517  qaa  26535  abelth  26655  efif1olem4  26761  eflog  26792  logef  26797  logeftb  26799  dvrelog  26853  dvlog  26867  cxpcn3  26964  efrlim  27185  eflgam  27260  wilthlem3  27285  basellem8  27303  lgsqrlem1  27561  noetasuplem4  27951  noetainflem4  27955  precsexlem1  28451  precsexlem2  28452  precsexlem3  28453  precsexlem4  28454  precsexlem5  28455  tgcgr4  28851  krippenlem  29018  colperpexlem1  29062  opphllem3  29081  lmiisolem  29156  axlowdimlem8  29354  axlowdimlem9  29355  axlowdimlem11  29357  axlowdimlem12  29358  axlowdimlem17  29363  ushgredgedg  29637  ushgredgedgloop  29639  subgruhgredgd  29692  vtxdlfgrval  29893  vtxd0nedgb  29896  vtxdushgrfvedg  29898  vtxdginducedm1lem3  29949  finsumvtxdg2size  29958  vtxdgoddnumeven  29961  isrgr  29967  fusgrregdegfi  29977  wlk1walk  30046  wlkres  30076  wlkp1lem5  30083  wlkp1lem6  30084  wlkp1lem7  30085  wlkp1lem8  30086  clwlkcompbp  30196  crctcshwlkn0lem4  30229  crctcshwlkn0lem5  30230  crctcshwlkn0lem6  30231  2wlkdlem3  30343  2wlkdlem8  30349  2wlkond  30353  umgr2adedgwlk  30361  1wlkdlem4  30558  1pthond  30562  2cycld  30572  wlk2v2elem2  30578  3wlkdlem3  30583  3wlkdlem8  30589  3cycld  30600  3cyclpd  30601  eucrctshift  30665  frgrncvvdeq  30731  frgrwopreglem2  30735  ex-fpar  30884  avril1  30885  vafval  31026  smfval  31028  0vfval  31029  nmcvfval  31030  vsfval  31056  hhssabloilem  31684  pjoc2i  31861  pjcji  32107  ho0val  32173  hoival  32178  adjbdlnb  32507  nmopcoadji  32524  opsqrlem2  32564  opsqrlem5  32567  hmopidmchi  32574  hmopidmpji  32575  pjinvari  32614  pjadj2coi  32627  pj3lem1  32629  pmtrprfv2  33472  cycpmco2lem7  33516  evl1fpws  33918  mplmulmvr  33993  evlextv  33996  esplyfval1  34027  esplyfvaln  34028  esplyind  34029  esplyindfv  34030  esplyfvn  34031  vietalem  34033  rtelextdg2lem  34180  constr0  34191  constrsuc  34192  constrlim  34193  2sqr3minply  34234  cos9thpiminplylem6  34241  madjusmdetlem1  34281  cnre2csqlem  34364  zzsnm  34413  rrhcn  34451  qqhre  34474  oms0  34752  omsmon  34753  omssubaddlem  34754  omssubadd  34755  eulerpart  34837  fib0  34854  fib1  34855  fibp1  34856  coinflippv  34939  gsumnunsn  34996  derangenlem  35700  kur14lem2  35736  kur14lem3  35737  kur14lem5  35739  kur14lem6  35740  txsconnlem  35769  cvmliftlem4  35817  cvmliftlem5  35818  satf0sucom  35902  satf0suc  35905  satf0op  35906  fmla  35910  satffunlem2lem2  35935  satfv0fvfmla0  35942  sate0  35944  funpartfv  36474  fullfunfv  36476  sumeq2si  36771  prodeq2si  36773  cbvprodvw2  36816  neibastop2lem  36928  dffinxpf  38088  ftc1cnnc  38400  heiborlem4  38523  heiborlem6  38525  cdlemk13  41684  cdlemk14  41686  cdlemk15  41687  cdlemk21N  41705  cdlemk20  41706  cdlemk56w  41805  lcfrlem1  42374  hdmapfval  42659  deg1gprod  42965  rabdiophlem2  43587  dnnumch1  43829  aomclem6  43844  mncn0  43924  aaitgo  43947  rngunsnply  43954  cytpval  43987  dssmapntrcls  44912  binomcxplemdvsum  45123  binomcxplemnotnn0  45124  binomcxp  45125  fvmpt2df  46045  fsumsermpt  46353  fmul01  46354  fmuldfeq  46357  fmul01lt1lem1  46358  fmul01lt1lem2  46359  lptioo2cn  46417  lptioo1cn  46418  limclner  46423  dvsinax  46685  fperdvper  46691  dvnmul  46715  dvnprodlem1  46718  dvnprodlem2  46719  dvnprodlem3  46720  itgsin0pilem1  46722  stoweidlem3  46775  stoweidlem17  46789  stoweidlem47  46819  fourierdlem42  46921  fourierdlem62  46940  fourierdlem80  46958  fourierdlem90  46968  fourierdlem92  46970  fourierdlem93  46971  fourierdlem103  46981  fourierdlem104  46982  fouriercnp  46998  sge0isum  47199  sge0seq  47218  ovnsubadd  47344  vonn0ioo  47459  vonn0icc  47460  smflimsup  47600  cjnpoly  47684  sinnpoly  47686  fcores  47862  fundcmpsurinjimaid  48218  isgrim  48705  gricushgr  48740  gpgprismgr4cycllem3  48920  gpgprismgr4cycllem6  48923  gpgprismgr4cycllem7  48924  gpgprismgr4cycllem10  48927  rhmsubcALTVlem2  49104  ply1mulgsum  49227  lineval  49231  lincvalpr  49255  lindslinindimp2lem4  49298  zlmodzxzldeplem3  49339  zlmodzxzldeplem4  49340  itcoval0mpt  49503  ackvalsuc1mpt  49515  ackval0  49517  ackval40  49530  ackval41a  49531  ackval42  49533  ackval50  49535  ehl2eudisval0  49562  2sphere0  49587  line2  49589  line2x  49591  line2y  49592  itscnhlinecirc02p  49622  oppcup  50042  natoppf  50064