Theorem fveq1i 6646

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

Syntax hints:   = wceq 1538  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332

This theorem is referenced by:  fveq12i  6651  fvun2  6730  fvopab3ig  6741  fvsnun1  6921  fvpr1  6929  fvpr2  6930  fvpr1g  6931  fvpr2g  6932  fvtp1  6934  fvtp2  6935  fvtp3  6936  fvtp1g  6937  fvtp2g  6938  fvtp3g  6939  fpropnf1  7003  fveqf1o  7037  ov  7273  ovigg  7274  ovg  7293  fvresex  7643  curry1  7782  curry2  7785  fsplitfpar  7797  suppsnop  7827  wfrlem5  7942  tfr2a  8014  rdgsucmptf  8047  rdgsucmptnf  8048  frsucmpt  8056  frsucmptn  8057  seqomlem1  8069  seqomlem3  8071  seqomlem4  8072  seqom0g  8075  seqomsuc  8076  unblem2  8755  inf3lemb  9072  inf3lemc  9073  trcl  9154  r10  9181  r1sucg  9182  r1limg  9184  infxpenc2  9433  aleph0  9477  alephlim  9478  alephsuc  9479  alephfplem1  9515  alephfplem2  9516  ackbij2lem3  9652  cfsmolem  9681  infpssrlem1  9714  infpssrlem2  9715  fin23lem34  9757  fin23lem35  9758  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  isf34lem5  9789  hsmexlem7  9834  axdclem2  9931  canthp1lem2  10064  wunex2  10149  wuncval2  10158  addpiord  10295  mulpiord  10296  addpqnq  10349  mulpqnq  10352  fseq1p1m1  12976  om2uz0i  13310  om2uzrdg  13319  uzrdg0i  13322  uzrdgsuci  13323  hashkf  13688  hashgval  13689  hashinf  13691  ccat1st1st  13975  revs1  14118  cats1fv  14212  shftidt  14433  cbvsum  15044  fsumss  15074  isumclim3  15106  isumsup2  15193  cbvprod  15261  fprodss  15294  iprodclim3  15346  fprodefsum  15440  ruclem4  15579  ruclem6  15580  ruclem7  15581  sadc0  15793  sadcp1  15794  sadcaddlem  15796  sadaddlem  15805  smup0  15818  smupp1  15819  algr0  15906  algrp1  15908  ndxarg  16500  strfv2d  16521  funcoppc  17137  fthepi  17190  homadm  17292  homacd  17293  prdsidlem  17935  prdsinvlem  18200  cayleylem2  18533  symggen  18590  pmtr3ncomlem1  18593  gsumval3  19020  gsumzaddlem  19034  gsumzmhm  19050  pgpfaclem1  19196  ringidval  19246  lidlval  19957  rspval  19958  lidlnegcl  19980  lpival  20011  znf1o  20243  eqcoe1ply1eq  20926  evls1val  20944  evl1val  20953  mat1dimmul  21081  mdetralt  21213  mdetunilem7  21223  decpmatid  21375  pmatcollpwscmatlem1  21394  cpmidpmat  21478  chcoeffeq  21491  restcls  21786  restntr  21787  upxp  22228  cnmetdval  23376  remetdval  23394  qdensere2  23402  pcoptcl  23626  pcopt  23627  pcopt2  23628  pcorevlem  23631  isncvsngp  23754  cnncvsabsnegdemo  23770  ovolfsval  24074  ovollb2lem  24092  ovolunlem1a  24100  ovoliunlem1  24106  ovoliun2  24110  ovolscalem1  24117  ovolicc2lem4  24124  mblvol  24134  ioombl1lem4  24165  uniioovol  24183  uniioombllem3  24189  0pval  24275  limccnp  24494  limccnp2  24495  dvcnvrelem2  24621  itgsubstlem  24651  ply1remlem  24763  plyrem  24901  qaa  24919  abelth  25036  efif1olem4  25137  eflog  25168  logef  25173  logeftb  25175  dvrelog  25228  dvlog  25242  cxpcn3  25337  efrlim  25555  eflgam  25630  wilthlem3  25655  basellem8  25673  lgsqrlem1  25930  tgcgr4  26325  krippenlem  26484  colperpexlem1  26524  opphllem3  26543  lmiisolem  26590  axlowdimlem8  26743  axlowdimlem9  26744  axlowdimlem11  26746  axlowdimlem12  26747  axlowdimlem17  26752  ushgredgedg  27019  ushgredgedgloop  27021  subgruhgredgd  27074  vtxdlfgrval  27275  vtxd0nedgb  27278  vtxdushgrfvedg  27280  vtxdginducedm1lem3  27331  finsumvtxdg2size  27340  vtxdgoddnumeven  27343  isrgr  27349  fusgrregdegfi  27359  wlk1walk  27428  wlkres  27460  wlkp1lem5  27467  wlkp1lem6  27468  wlkp1lem7  27469  wlkp1lem8  27470  clwlkcompbp  27571  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem6  27601  2wlkdlem3  27713  2wlkdlem8  27719  2wlkond  27723  umgr2adedgwlk  27731  1wlkdlem4  27925  1pthond  27929  wlk2v2elem2  27941  3wlkdlem3  27946  3wlkdlem8  27952  3cycld  27963  3cyclpd  27964  eucrctshift  28028  frgrncvvdeq  28094  frgrwopreglem2  28098  ex-fpar  28247  avril1  28248  vafval  28386  smfval  28388  0vfval  28389  nmcvfval  28390  vsfval  28416  hhssabloilem  29044  pjoc2i  29221  pjcji  29467  ho0val  29533  hoival  29538  adjbdlnb  29867  nmopcoadji  29884  opsqrlem2  29924  opsqrlem5  29927  hmopidmchi  29934  hmopidmpji  29935  pjinvari  29974  pjadj2coi  29987  pj3lem1  29989  funcnvmpt  30430  pmtrprfv2  30782  cycpmco2lem7  30824  rgmoddim  31096  madjusmdetlem1  31180  cnre2csqlem  31263  zzsnm  31312  rrhcn  31348  qqhre  31371  oms0  31665  omsmon  31666  omssubaddlem  31667  omssubadd  31668  eulerpart  31750  fib0  31767  fib1  31768  fibp1  31769  coinflippv  31851  gsumnunsn  31921  2cycld  32498  derangenlem  32531  kur14lem2  32567  kur14lem3  32568  kur14lem5  32570  kur14lem6  32571  txsconnlem  32600  cvmliftlem4  32648  cvmliftlem5  32649  satf0sucom  32733  satf0suc  32736  satf0op  32737  fmla  32741  satffunlem2lem2  32766  satfv0fvfmla0  32773  sate0  32775  trpredmintr  33183  trpred0  33188  frrlem12  33247  fprlem1  33250  frrlem15  33255  noetalem3  33332  funpartfv  33519  fullfunfv  33521  neibastop2lem  33821  dffinxpf  34802  ftc1cnnc  35129  heiborlem4  35252  heiborlem6  35254  cdlemk13  38148  cdlemk14  38150  cdlemk15  38151  cdlemk21N  38169  cdlemk20  38170  cdlemk56w  38269  lcfrlem1  38838  hdmapfval  39123  rabdiophlem2  39743  dnnumch1  39988  aomclem6  40003  mncn0  40083  aaitgo  40106  rngunsnply  40117  cytpval  40153  dssmapntrcls  40831  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  binomcxp  41061  fvcod  41858  fsumsermpt  42221  fmul01  42222  fmuldfeq  42225  fmul01lt1lem1  42226  fmul01lt1lem2  42227  lptioo2cn  42287  lptioo1cn  42288  limclner  42293  dvsinax  42555  fperdvper  42561  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  itgsin0pilem1  42592  stoweidlem3  42645  stoweidlem17  42659  stoweidlem47  42689  fourierdlem42  42791  fourierdlem62  42810  fourierdlem80  42828  fourierdlem90  42838  fourierdlem92  42840  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  fouriercnp  42868  sge0isum  43066  sge0seq  43085  ovnsubadd  43211  vonn0ioo  43326  vonn0icc  43327  smflimsup  43459  fundcmpsurinjimaid  43928  isomushgr  44344  rhmsubclem2  44711  rhmsubcALTVlem2  44729  ply1mulgsum  44798  lineval  44802  lincvalpr  44827  lindslinindimp2lem4  44870  zlmodzxzldeplem3  44911  zlmodzxzldeplem4  44912  itcoval0mpt  45080  ackvalsuc1mpt  45092  ackval0  45094  ackval40  45107  ackval41a  45108  ackval42  45110  ackval50  45112  ehl2eudisval0  45139  2sphere0  45164  line2  45166  line2x  45168  line2y  45169  itscnhlinecirc02p  45199