Theorem fveq1i 6890

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

Syntax hints:   = wceq 1542  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549

This theorem is referenced by:  fveq12i  6895  fvun2  6981  fvopab3ig  6992  fvsnun1  7177  fvpr1g  7185  fvpr2g  7186  fvpr2gOLD  7187  fvpr1OLD  7189  fvpr2OLD  7191  fvtp1  7193  fvtp2  7194  fvtp3  7195  fvtp1g  7196  fvtp2g  7197  fvtp3g  7198  fpropnf1  7263  fveqf1o  7298  ov  7549  ovigg  7550  ovg  7569  fvresex  7943  curry1  8087  curry2  8090  fsplitfpar  8101  suppsnop  8160  frrlem12  8279  fprlem1  8282  wfrlem5OLD  8310  tfr2a  8392  rdgsucmptf  8425  rdgsucmptnf  8426  frsucmpt  8435  frsucmptn  8436  seqomlem1  8447  seqomlem3  8449  seqomlem4  8450  seqom0g  8453  seqomsuc  8454  unblem2  9293  inf3lemb  9617  inf3lemc  9618  ttrclselem1  9717  ttrclselem2  9718  trcl  9720  frrlem15  9749  r10  9760  r1sucg  9761  r1limg  9763  infxpenc2  10014  aleph0  10058  alephlim  10059  alephsuc  10060  alephfplem1  10096  alephfplem2  10097  ackbij2lem3  10233  cfsmolem  10262  infpssrlem1  10295  infpssrlem2  10296  fin23lem34  10338  fin23lem35  10339  isf32lem6  10350  isf32lem7  10351  isf32lem8  10352  isf34lem5  10370  hsmexlem7  10415  axdclem2  10512  canthp1lem2  10645  wunex2  10730  wuncval2  10739  addpiord  10876  mulpiord  10877  addpqnq  10930  mulpqnq  10933  fseq1p1m1  13572  om2uz0i  13909  om2uzrdg  13918  uzrdg0i  13921  uzrdgsuci  13922  hashkf  14289  hashgval  14290  hashinf  14292  ccat1st1st  14575  revs1  14712  cats1fv  14807  shftidt  15026  cbvsum  15638  fsumss  15668  isumclim3  15702  isumsup2  15789  cbvprod  15856  fprodss  15889  iprodclim3  15941  fprodefsum  16035  ruclem4  16174  ruclem6  16175  ruclem7  16176  sadc0  16392  sadcp1  16393  sadcaddlem  16395  sadaddlem  16404  smup0  16417  smupp1  16418  algr0  16506  algrp1  16508  ndxarg  17126  strfv2d  17132  funcoppc  17822  fthepi  17876  homadm  17987  homacd  17988  prdsidlem  18654  prdsinvlem  18929  cayleylem2  19276  symggen  19333  pmtr3ncomlem1  19336  gsumval3  19770  gsumzaddlem  19784  gsumzmhm  19800  pgpfaclem1  19946  ringidval  20001  lidlval  20807  rspval  20808  lidlnegcl  20830  lpival  20876  znf1o  21099  eqcoe1ply1eq  21813  evls1val  21831  evl1val  21840  mat1dimmul  21970  mdetralt  22102  mdetunilem7  22112  decpmatid  22264  pmatcollpwscmatlem1  22283  cpmidpmat  22367  chcoeffeq  22380  restcls  22677  restntr  22678  upxp  23119  cnmetdval  24279  remetdval  24297  qdensere2  24305  pcoptcl  24529  pcopt  24530  pcopt2  24531  pcorevlem  24534  isncvsngp  24658  cnncvsabsnegdemo  24674  ovolfsval  24979  ovollb2lem  24997  ovolunlem1a  25005  ovoliunlem1  25011  ovoliun2  25015  ovolscalem1  25022  ovolicc2lem4  25029  mblvol  25039  ioombl1lem4  25070  uniioovol  25088  uniioombllem3  25094  0pval  25180  limccnp  25400  limccnp2  25401  dvcnvrelem2  25527  itgsubstlem  25557  ply1remlem  25672  plyrem  25810  qaa  25828  abelth  25945  efif1olem4  26046  eflog  26077  logef  26082  logeftb  26084  dvrelog  26137  dvlog  26151  cxpcn3  26246  efrlim  26464  eflgam  26539  wilthlem3  26564  basellem8  26582  lgsqrlem1  26839  noetasuplem4  27229  noetainflem4  27233  precsexlem1  27643  precsexlem2  27644  precsexlem3  27645  precsexlem4  27646  precsexlem5  27647  tgcgr4  27772  krippenlem  27931  colperpexlem1  27971  opphllem3  27990  lmiisolem  28037  axlowdimlem8  28197  axlowdimlem9  28198  axlowdimlem11  28200  axlowdimlem12  28201  axlowdimlem17  28206  ushgredgedg  28476  ushgredgedgloop  28478  subgruhgredgd  28531  vtxdlfgrval  28732  vtxd0nedgb  28735  vtxdushgrfvedg  28737  vtxdginducedm1lem3  28788  finsumvtxdg2size  28797  vtxdgoddnumeven  28800  isrgr  28806  fusgrregdegfi  28816  wlk1walk  28886  wlkres  28917  wlkp1lem5  28924  wlkp1lem6  28925  wlkp1lem7  28926  wlkp1lem8  28927  clwlkcompbp  29029  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  crctcshwlkn0lem6  29059  2wlkdlem3  29171  2wlkdlem8  29177  2wlkond  29181  umgr2adedgwlk  29189  1wlkdlem4  29383  1pthond  29387  wlk2v2elem2  29399  3wlkdlem3  29404  3wlkdlem8  29410  3cycld  29421  3cyclpd  29422  eucrctshift  29486  frgrncvvdeq  29552  frgrwopreglem2  29556  ex-fpar  29705  avril1  29706  vafval  29844  smfval  29846  0vfval  29847  nmcvfval  29848  vsfval  29874  hhssabloilem  30502  pjoc2i  30679  pjcji  30925  ho0val  30991  hoival  30996  adjbdlnb  31325  nmopcoadji  31342  opsqrlem2  31382  opsqrlem5  31385  hmopidmchi  31392  hmopidmpji  31393  pjinvari  31432  pjadj2coi  31445  pj3lem1  31447  funcnvmpt  31880  pmtrprfv2  32237  cycpmco2lem7  32279  ply1ascl0  32641  ply1ascl1  32642  rgmoddimOLD  32684  madjusmdetlem1  32796  cnre2csqlem  32879  zzsnm  32928  rrhcn  32966  qqhre  32989  oms0  33285  omsmon  33286  omssubaddlem  33287  omssubadd  33288  eulerpart  33370  fib0  33387  fib1  33388  fibp1  33389  coinflippv  33471  gsumnunsn  33541  2cycld  34118  derangenlem  34151  kur14lem2  34187  kur14lem3  34188  kur14lem5  34190  kur14lem6  34191  txsconnlem  34220  cvmliftlem4  34268  cvmliftlem5  34269  satf0sucom  34353  satf0suc  34356  satf0op  34357  fmla  34361  satffunlem2lem2  34386  satfv0fvfmla0  34393  sate0  34395  funpartfv  34906  fullfunfv  34908  neibastop2lem  35234  dffinxpf  36255  ftc1cnnc  36549  heiborlem4  36671  heiborlem6  36673  cdlemk13  39712  cdlemk14  39714  cdlemk15  39715  cdlemk21N  39733  cdlemk20  39734  cdlemk56w  39833  lcfrlem1  40402  hdmapfval  40687  evlsevl  41141  selvvvval  41155  rabdiophlem2  41526  dnnumch1  41772  aomclem6  41787  mncn0  41867  aaitgo  41890  rngunsnply  41901  cytpval  41937  dssmapntrcls  42865  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  binomcxp  43102  fvcod  43912  fvmpt2df  43964  fsumsermpt  44282  fmul01  44283  fmuldfeq  44286  fmul01lt1lem1  44287  fmul01lt1lem2  44288  lptioo2cn  44348  lptioo1cn  44349  limclner  44354  dvsinax  44616  fperdvper  44622  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  dvnprodlem3  44651  itgsin0pilem1  44653  stoweidlem3  44706  stoweidlem17  44720  stoweidlem47  44750  fourierdlem42  44852  fourierdlem62  44871  fourierdlem80  44889  fourierdlem90  44899  fourierdlem92  44901  fourierdlem93  44902  fourierdlem103  44912  fourierdlem104  44913  fouriercnp  44929  sge0isum  45130  sge0seq  45149  ovnsubadd  45275  vonn0ioo  45390  vonn0icc  45391  smflimsup  45531  fcores  45764  fundcmpsurinjimaid  46066  isomushgr  46481  rhmsubclem2  46939  rhmsubcALTVlem2  46957  ply1mulgsum  47025  lineval  47029  lincvalpr  47053  lindslinindimp2lem4  47096  zlmodzxzldeplem3  47137  zlmodzxzldeplem4  47138  itcoval0mpt  47306  ackvalsuc1mpt  47318  ackval0  47320  ackval40  47333  ackval41a  47334  ackval42  47336  ackval50  47338  ehl2eudisval0  47365  2sphere0  47390  line2  47392  line2x  47394  line2y  47395  itscnhlinecirc02p  47425