Theorem fveq1i 6826

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

Syntax hints:   = wceq 1540  ‘cfv 6479

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-uni 4853  df-br 5093  df-iota 6431  df-fv 6487

This theorem is referenced by:  fveq12i  6831  fvun2  6916  fvopab3ig  6927  fvsnun1  7110  fvpr1g  7118  fvpr2g  7119  fvpr2gOLD  7120  fvpr1OLD  7122  fvpr2OLD  7124  fvtp1  7126  fvtp2  7127  fvtp3  7128  fvtp1g  7129  fvtp2g  7130  fvtp3g  7131  fpropnf1  7196  fveqf1o  7231  ov  7479  ovigg  7480  ovg  7499  fvresex  7870  curry1  8012  curry2  8015  fsplitfpar  8026  suppsnop  8064  frrlem12  8183  fprlem1  8186  wfrlem5OLD  8214  tfr2a  8296  rdgsucmptf  8329  rdgsucmptnf  8330  frsucmpt  8339  frsucmptn  8340  seqomlem1  8351  seqomlem3  8353  seqomlem4  8354  seqom0g  8357  seqomsuc  8358  unblem2  9161  inf3lemb  9482  inf3lemc  9483  ttrclselem1  9582  ttrclselem2  9583  trcl  9585  frrlem15  9614  r10  9625  r1sucg  9626  r1limg  9628  infxpenc2  9879  aleph0  9923  alephlim  9924  alephsuc  9925  alephfplem1  9961  alephfplem2  9962  ackbij2lem3  10098  cfsmolem  10127  infpssrlem1  10160  infpssrlem2  10161  fin23lem34  10203  fin23lem35  10204  isf32lem6  10215  isf32lem7  10216  isf32lem8  10217  isf34lem5  10235  hsmexlem7  10280  axdclem2  10377  canthp1lem2  10510  wunex2  10595  wuncval2  10604  addpiord  10741  mulpiord  10742  addpqnq  10795  mulpqnq  10798  fseq1p1m1  13431  om2uz0i  13768  om2uzrdg  13777  uzrdg0i  13780  uzrdgsuci  13781  hashkf  14147  hashgval  14148  hashinf  14150  ccat1st1st  14433  revs1  14576  cats1fv  14671  shftidt  14892  cbvsum  15506  fsumss  15536  isumclim3  15570  isumsup2  15657  cbvprod  15724  fprodss  15757  iprodclim3  15809  fprodefsum  15903  ruclem4  16042  ruclem6  16043  ruclem7  16044  sadc0  16260  sadcp1  16261  sadcaddlem  16263  sadaddlem  16272  smup0  16285  smupp1  16286  algr0  16374  algrp1  16376  ndxarg  16994  strfv2d  17000  funcoppc  17687  fthepi  17741  homadm  17852  homacd  17853  prdsidlem  18514  prdsinvlem  18780  cayleylem2  19117  symggen  19174  pmtr3ncomlem1  19177  gsumval3  19603  gsumzaddlem  19617  gsumzmhm  19633  pgpfaclem1  19779  ringidval  19834  lidlval  20568  rspval  20569  lidlnegcl  20591  lpival  20622  znf1o  20865  eqcoe1ply1eq  21574  evls1val  21592  evl1val  21601  mat1dimmul  21731  mdetralt  21863  mdetunilem7  21873  decpmatid  22025  pmatcollpwscmatlem1  22044  cpmidpmat  22128  chcoeffeq  22141  restcls  22438  restntr  22439  upxp  22880  cnmetdval  24040  remetdval  24058  qdensere2  24066  pcoptcl  24290  pcopt  24291  pcopt2  24292  pcorevlem  24295  isncvsngp  24419  cnncvsabsnegdemo  24435  ovolfsval  24740  ovollb2lem  24758  ovolunlem1a  24766  ovoliunlem1  24772  ovoliun2  24776  ovolscalem1  24783  ovolicc2lem4  24790  mblvol  24800  ioombl1lem4  24831  uniioovol  24849  uniioombllem3  24855  0pval  24941  limccnp  25161  limccnp2  25162  dvcnvrelem2  25288  itgsubstlem  25318  ply1remlem  25433  plyrem  25571  qaa  25589  abelth  25706  efif1olem4  25807  eflog  25838  logef  25843  logeftb  25845  dvrelog  25898  dvlog  25912  cxpcn3  26007  efrlim  26225  eflgam  26300  wilthlem3  26325  basellem8  26343  lgsqrlem1  26600  noetasuplem4  26990  noetainflem4  26994  tgcgr4  27181  krippenlem  27340  colperpexlem1  27380  opphllem3  27399  lmiisolem  27446  axlowdimlem8  27606  axlowdimlem9  27607  axlowdimlem11  27609  axlowdimlem12  27610  axlowdimlem17  27615  ushgredgedg  27885  ushgredgedgloop  27887  subgruhgredgd  27940  vtxdlfgrval  28141  vtxd0nedgb  28144  vtxdushgrfvedg  28146  vtxdginducedm1lem3  28197  finsumvtxdg2size  28206  vtxdgoddnumeven  28209  isrgr  28215  fusgrregdegfi  28225  wlk1walk  28295  wlkres  28326  wlkp1lem5  28333  wlkp1lem6  28334  wlkp1lem7  28335  wlkp1lem8  28336  clwlkcompbp  28438  crctcshwlkn0lem4  28466  crctcshwlkn0lem5  28467  crctcshwlkn0lem6  28468  2wlkdlem3  28580  2wlkdlem8  28586  2wlkond  28590  umgr2adedgwlk  28598  1wlkdlem4  28792  1pthond  28796  wlk2v2elem2  28808  3wlkdlem3  28813  3wlkdlem8  28819  3cycld  28830  3cyclpd  28831  eucrctshift  28895  frgrncvvdeq  28961  frgrwopreglem2  28965  ex-fpar  29114  avril1  29115  vafval  29253  smfval  29255  0vfval  29256  nmcvfval  29257  vsfval  29283  hhssabloilem  29911  pjoc2i  30088  pjcji  30334  ho0val  30400  hoival  30405  adjbdlnb  30734  nmopcoadji  30751  opsqrlem2  30791  opsqrlem5  30794  hmopidmchi  30801  hmopidmpji  30802  pjinvari  30841  pjadj2coi  30854  pj3lem1  30856  funcnvmpt  31291  pmtrprfv2  31644  cycpmco2lem7  31686  rgmoddim  31991  madjusmdetlem1  32075  cnre2csqlem  32158  zzsnm  32207  rrhcn  32245  qqhre  32268  oms0  32564  omsmon  32565  omssubaddlem  32566  omssubadd  32567  eulerpart  32649  fib0  32666  fib1  32667  fibp1  32668  coinflippv  32750  gsumnunsn  32820  2cycld  33399  derangenlem  33432  kur14lem2  33468  kur14lem3  33469  kur14lem5  33471  kur14lem6  33472  txsconnlem  33501  cvmliftlem4  33549  cvmliftlem5  33550  satf0sucom  33634  satf0suc  33637  satf0op  33638  fmla  33642  satffunlem2lem2  33667  satfv0fvfmla0  33674  sate0  33676  funpartfv  34343  fullfunfv  34345  neibastop2lem  34645  dffinxpf  35669  ftc1cnnc  35962  heiborlem4  36085  heiborlem6  36087  cdlemk13  39128  cdlemk14  39130  cdlemk15  39131  cdlemk21N  39149  cdlemk20  39150  cdlemk56w  39249  lcfrlem1  39818  hdmapfval  40103  mplascl0  40538  rabdiophlem2  40894  dnnumch1  41140  aomclem6  41155  mncn0  41235  aaitgo  41258  rngunsnply  41269  cytpval  41305  dssmapntrcls  42067  binomcxplemdvsum  42302  binomcxplemnotnn0  42303  binomcxp  42304  fvcod  43102  fsumsermpt  43464  fmul01  43465  fmuldfeq  43468  fmul01lt1lem1  43469  fmul01lt1lem2  43470  lptioo2cn  43530  lptioo1cn  43531  limclner  43536  dvsinax  43798  fperdvper  43804  dvnmul  43828  dvnprodlem1  43831  dvnprodlem2  43832  dvnprodlem3  43833  itgsin0pilem1  43835  stoweidlem3  43888  stoweidlem17  43902  stoweidlem47  43932  fourierdlem42  44034  fourierdlem62  44053  fourierdlem80  44071  fourierdlem90  44081  fourierdlem92  44083  fourierdlem93  44084  fourierdlem103  44094  fourierdlem104  44095  fouriercnp  44111  sge0isum  44310  sge0seq  44329  ovnsubadd  44455  vonn0ioo  44570  vonn0icc  44571  smflimsup  44711  fcores  44920  fundcmpsurinjimaid  45222  isomushgr  45637  rhmsubclem2  46004  rhmsubcALTVlem2  46022  ply1mulgsum  46090  lineval  46094  lincvalpr  46118  lindslinindimp2lem4  46161  zlmodzxzldeplem3  46202  zlmodzxzldeplem4  46203  itcoval0mpt  46371  ackvalsuc1mpt  46383  ackval0  46385  ackval40  46398  ackval41a  46399  ackval42  46401  ackval50  46403  ehl2eudisval0  46430  2sphere0  46455  line2  46457  line2x  46459  line2y  46460  itscnhlinecirc02p  46490