Theorem fveq1i 6673

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

Syntax hints:   = wceq 1537  ‘cfv 6357

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365

This theorem is referenced by:  fveq12i  6678  fvun2  6757  fvopab3ig  6766  fvsnun1  6946  fvpr1  6954  fvpr2  6955  fvpr1g  6956  fvpr2g  6957  fvtp1  6959  fvtp2  6960  fvtp3  6961  fvtp1g  6962  fvtp2g  6963  fvtp3g  6964  fpropnf1  7027  fveqf1o  7060  ov  7296  ovigg  7297  ovg  7315  fvresex  7663  curry1  7801  curry2  7804  fsplitfpar  7816  suppsnop  7846  wfrlem5  7961  tfr2a  8033  rdgsucmptf  8066  rdgsucmptnf  8067  frsucmpt  8075  frsucmptn  8076  seqomlem1  8088  seqomlem3  8090  seqomlem4  8091  seqom0g  8094  seqomsuc  8095  unblem2  8773  inf3lemb  9090  inf3lemc  9091  trcl  9172  r10  9199  r1sucg  9200  r1limg  9202  infxpenc2  9450  aleph0  9494  alephlim  9495  alephsuc  9496  alephfplem1  9532  alephfplem2  9533  ackbij2lem3  9665  cfsmolem  9694  infpssrlem1  9727  infpssrlem2  9728  fin23lem34  9770  fin23lem35  9771  isf32lem6  9782  isf32lem7  9783  isf32lem8  9784  isf34lem5  9802  hsmexlem7  9847  axdclem2  9944  canthp1lem2  10077  wunex2  10162  wuncval2  10171  addpiord  10308  mulpiord  10309  addpqnq  10362  mulpqnq  10365  fseq1p1m1  12984  om2uz0i  13318  om2uzrdg  13327  uzrdg0i  13330  uzrdgsuci  13331  hashkf  13695  hashgval  13696  hashinf  13698  ccat1st1st  13986  revs1  14129  cats1fv  14223  shftidt  14443  cbvsum  15054  fsumss  15084  isumclim3  15116  isumsup2  15203  cbvprod  15271  fprodss  15304  iprodclim3  15356  fprodefsum  15450  ruclem4  15589  ruclem6  15590  ruclem7  15591  sadc0  15805  sadcp1  15806  sadcaddlem  15808  sadaddlem  15817  smup0  15830  smupp1  15831  algr0  15918  algrp1  15920  ndxarg  16510  strfv2d  16531  funcoppc  17147  fthepi  17200  homadm  17302  homacd  17303  prdsidlem  17945  prdsinvlem  18210  cayleylem2  18543  symggen  18600  pmtr3ncomlem1  18603  gsumval3  19029  gsumzaddlem  19043  gsumzmhm  19059  pgpfaclem1  19205  ringidval  19255  lidlval  19966  rspval  19967  lidlnegcl  19989  lpival  20020  eqcoe1ply1eq  20467  evls1val  20485  evl1val  20494  znf1o  20700  mat1dimmul  21087  mdetralt  21219  mdetunilem7  21229  decpmatid  21380  pmatcollpwscmatlem1  21399  cpmidpmat  21483  chcoeffeq  21496  restcls  21791  restntr  21792  upxp  22233  cnmetdval  23381  remetdval  23399  qdensere2  23407  pcoptcl  23627  pcopt  23628  pcopt2  23629  pcorevlem  23632  isncvsngp  23755  cnncvsabsnegdemo  23771  ovolfsval  24073  ovollb2lem  24091  ovolunlem1a  24099  ovoliunlem1  24105  ovoliun2  24109  ovolscalem1  24116  ovolicc2lem4  24123  mblvol  24133  ioombl1lem4  24164  uniioovol  24182  uniioombllem3  24188  0pval  24274  limccnp  24491  limccnp2  24492  dvcnvrelem2  24617  itgsubstlem  24647  ply1remlem  24758  plyrem  24896  qaa  24914  abelth  25031  efif1olem4  25131  eflog  25162  logef  25167  logeftb  25169  dvrelog  25222  dvlog  25236  cxpcn3  25331  efrlim  25549  eflgam  25624  wilthlem3  25649  basellem8  25667  lgsqrlem1  25924  tgcgr4  26319  krippenlem  26478  colperpexlem1  26518  opphllem3  26537  lmiisolem  26584  axlowdimlem8  26737  axlowdimlem9  26738  axlowdimlem11  26740  axlowdimlem12  26741  axlowdimlem17  26746  ushgredgedg  27013  ushgredgedgloop  27015  subgruhgredgd  27068  vtxdlfgrval  27269  vtxd0nedgb  27272  vtxdushgrfvedg  27274  vtxdginducedm1lem3  27325  finsumvtxdg2size  27334  vtxdgoddnumeven  27337  isrgr  27343  fusgrregdegfi  27353  wlk1walk  27422  wlkres  27454  wlkp1lem5  27461  wlkp1lem6  27462  wlkp1lem7  27463  wlkp1lem8  27464  clwlkcompbp  27565  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshwlkn0lem6  27595  2wlkdlem3  27708  2wlkdlem8  27714  2wlkond  27718  umgr2adedgwlk  27726  1wlkdlem4  27921  1pthond  27925  wlk2v2elem2  27937  3wlkdlem3  27942  3wlkdlem8  27948  3cycld  27959  3cyclpd  27960  eucrctshift  28024  frgrncvvdeq  28090  frgrwopreglem2  28094  ex-fpar  28243  avril1  28244  vafval  28382  smfval  28384  0vfval  28385  nmcvfval  28386  vsfval  28412  hhssabloilem  29040  pjoc2i  29217  pjcji  29463  ho0val  29529  hoival  29534  adjbdlnb  29863  nmopcoadji  29880  opsqrlem2  29920  opsqrlem5  29923  hmopidmchi  29930  hmopidmpji  29931  pjinvari  29970  pjadj2coi  29983  pj3lem1  29985  funcnvmpt  30414  pmtrprfv2  30734  cycpmco2lem7  30776  rgmoddim  31010  madjusmdetlem1  31094  cnre2csqlem  31155  zzsnm  31204  rrhcn  31240  qqhre  31263  oms0  31557  omsmon  31558  omssubaddlem  31559  omssubadd  31560  eulerpart  31642  fib0  31659  fib1  31660  fibp1  31661  coinflippv  31743  gsumnunsn  31813  2cycld  32387  derangenlem  32420  kur14lem2  32456  kur14lem3  32457  kur14lem5  32459  kur14lem6  32460  txsconnlem  32489  cvmliftlem4  32537  cvmliftlem5  32538  satf0sucom  32622  satf0suc  32625  satf0op  32626  fmla  32630  satffunlem2lem2  32655  satfv0fvfmla0  32662  sate0  32664  trpredmintr  33072  trpred0  33077  frrlem12  33136  fprlem1  33139  frrlem15  33144  noetalem3  33221  funpartfv  33408  fullfunfv  33410  neibastop2lem  33710  dffinxpf  34668  ftc1cnnc  34968  heiborlem4  35094  heiborlem6  35096  cdlemk13  37990  cdlemk14  37992  cdlemk15  37993  cdlemk21N  38011  cdlemk20  38012  cdlemk56w  38111  lcfrlem1  38680  hdmapfval  38965  rabdiophlem2  39406  dnnumch1  39651  aomclem6  39666  mncn0  39746  aaitgo  39769  rngunsnply  39780  cytpval  39816  dssmapntrcls  40485  binomcxplemdvsum  40694  binomcxplemnotnn0  40695  binomcxp  40696  fvcod  41499  fsumsermpt  41867  fmul01  41868  fmuldfeq  41871  fmul01lt1lem1  41872  fmul01lt1lem2  41873  lptioo2cn  41933  lptioo1cn  41934  limclner  41939  dvsinax  42204  fperdvper  42210  dvnmul  42235  dvnprodlem1  42238  dvnprodlem2  42239  dvnprodlem3  42240  itgsin0pilem1  42242  stoweidlem3  42295  stoweidlem17  42309  stoweidlem47  42339  fourierdlem42  42441  fourierdlem62  42460  fourierdlem80  42478  fourierdlem90  42488  fourierdlem92  42490  fourierdlem93  42491  fourierdlem103  42501  fourierdlem104  42502  fouriercnp  42518  sge0isum  42716  sge0seq  42735  ovnsubadd  42861  vonn0ioo  42976  vonn0icc  42977  smflimsup  43109  fundcmpsurinjimaid  43578  isomushgr  43998  rhmsubclem2  44365  rhmsubcALTVlem2  44383  ply1mulgsum  44451  lineval  44455  lincvalpr  44480  lindslinindimp2lem4  44523  zlmodzxzldeplem3  44564  zlmodzxzldeplem4  44565  ehl2eudisval0  44719  2sphere0  44744  line2  44746  line2x  44748  line2y  44749  itscnhlinecirc02p  44779