Theorem fveq1i 6891

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

Syntax hints:   = wceq 1539  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550

This theorem is referenced by:  fveq12i  6896  fvun2  6982  fvopab3ig  6993  fvsnun1  7181  fvpr1g  7189  fvpr2g  7190  fvpr2gOLD  7191  fvpr1OLD  7193  fvpr2OLD  7195  fvtp1  7197  fvtp2  7198  fvtp3  7199  fvtp1g  7200  fvtp2g  7201  fvtp3g  7202  fpropnf1  7268  fveqf1o  7303  ov  7554  ovigg  7555  ovg  7574  fvresex  7948  curry1  8092  curry2  8095  fsplitfpar  8106  suppsnop  8165  frrlem12  8284  fprlem1  8287  wfrlem5OLD  8315  tfr2a  8397  rdgsucmptf  8430  rdgsucmptnf  8431  frsucmpt  8440  frsucmptn  8441  seqomlem1  8452  seqomlem3  8454  seqomlem4  8455  seqom0g  8458  seqomsuc  8459  unblem2  9298  inf3lemb  9622  inf3lemc  9623  ttrclselem1  9722  ttrclselem2  9723  trcl  9725  frrlem15  9754  r10  9765  r1sucg  9766  r1limg  9768  infxpenc2  10019  aleph0  10063  alephlim  10064  alephsuc  10065  alephfplem1  10101  alephfplem2  10102  ackbij2lem3  10238  cfsmolem  10267  infpssrlem1  10300  infpssrlem2  10301  fin23lem34  10343  fin23lem35  10344  isf32lem6  10355  isf32lem7  10356  isf32lem8  10357  isf34lem5  10375  hsmexlem7  10420  axdclem2  10517  canthp1lem2  10650  wunex2  10735  wuncval2  10744  addpiord  10881  mulpiord  10882  addpqnq  10935  mulpqnq  10938  fseq1p1m1  13579  om2uz0i  13916  om2uzrdg  13925  uzrdg0i  13928  uzrdgsuci  13929  hashkf  14296  hashgval  14297  hashinf  14299  ccat1st1st  14582  revs1  14719  cats1fv  14814  shftidt  15033  cbvsum  15645  fsumss  15675  isumclim3  15709  isumsup2  15796  cbvprod  15863  fprodss  15896  iprodclim3  15948  fprodefsum  16042  ruclem4  16181  ruclem6  16182  ruclem7  16183  sadc0  16399  sadcp1  16400  sadcaddlem  16402  sadaddlem  16411  smup0  16424  smupp1  16425  algr0  16513  algrp1  16515  ndxarg  17133  strfv2d  17139  funcoppc  17829  fthepi  17883  homadm  17994  homacd  17995  prdsidlem  18691  prdsinvlem  18968  cayleylem2  19322  symggen  19379  pmtr3ncomlem1  19382  gsumval3  19816  gsumzaddlem  19830  gsumzmhm  19846  pgpfaclem1  19992  ringidval  20077  lidlval  20959  rspval  20960  lidlnegcl  20986  lpival  21083  znf1o  21326  eqcoe1ply1eq  22041  evls1val  22059  evl1val  22068  mat1dimmul  22198  mdetralt  22330  mdetunilem7  22340  decpmatid  22492  pmatcollpwscmatlem1  22511  cpmidpmat  22595  chcoeffeq  22608  restcls  22905  restntr  22906  upxp  23347  cnmetdval  24507  remetdval  24525  qdensere2  24533  pcoptcl  24768  pcopt  24769  pcopt2  24770  pcorevlem  24773  isncvsngp  24897  cnncvsabsnegdemo  24913  ovolfsval  25219  ovollb2lem  25237  ovolunlem1a  25245  ovoliunlem1  25251  ovoliun2  25255  ovolscalem1  25262  ovolicc2lem4  25269  mblvol  25279  ioombl1lem4  25310  uniioovol  25328  uniioombllem3  25334  0pval  25420  limccnp  25640  limccnp2  25641  dvcnvrelem2  25770  itgsubstlem  25800  ply1remlem  25915  plyrem  26054  qaa  26072  abelth  26189  efif1olem4  26290  eflog  26321  logef  26326  logeftb  26328  dvrelog  26381  dvlog  26395  cxpcn3  26492  efrlim  26710  eflgam  26785  wilthlem3  26810  basellem8  26828  lgsqrlem1  27085  noetasuplem4  27475  noetainflem4  27479  precsexlem1  27892  precsexlem2  27893  precsexlem3  27894  precsexlem4  27895  precsexlem5  27896  tgcgr4  28049  krippenlem  28208  colperpexlem1  28248  opphllem3  28267  lmiisolem  28314  axlowdimlem8  28474  axlowdimlem9  28475  axlowdimlem11  28477  axlowdimlem12  28478  axlowdimlem17  28483  ushgredgedg  28753  ushgredgedgloop  28755  subgruhgredgd  28808  vtxdlfgrval  29009  vtxd0nedgb  29012  vtxdushgrfvedg  29014  vtxdginducedm1lem3  29065  finsumvtxdg2size  29074  vtxdgoddnumeven  29077  isrgr  29083  fusgrregdegfi  29093  wlk1walk  29163  wlkres  29194  wlkp1lem5  29201  wlkp1lem6  29202  wlkp1lem7  29203  wlkp1lem8  29204  clwlkcompbp  29306  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  crctcshwlkn0lem6  29336  2wlkdlem3  29448  2wlkdlem8  29454  2wlkond  29458  umgr2adedgwlk  29466  1wlkdlem4  29660  1pthond  29664  wlk2v2elem2  29676  3wlkdlem3  29681  3wlkdlem8  29687  3cycld  29698  3cyclpd  29699  eucrctshift  29763  frgrncvvdeq  29829  frgrwopreglem2  29833  ex-fpar  29982  avril1  29983  vafval  30123  smfval  30125  0vfval  30126  nmcvfval  30127  vsfval  30153  hhssabloilem  30781  pjoc2i  30958  pjcji  31204  ho0val  31270  hoival  31275  adjbdlnb  31604  nmopcoadji  31621  opsqrlem2  31661  opsqrlem5  31664  hmopidmchi  31671  hmopidmpji  31672  pjinvari  31711  pjadj2coi  31724  pj3lem1  31726  funcnvmpt  32159  pmtrprfv2  32519  cycpmco2lem7  32561  ply1ascl0  32926  ply1ascl1  32927  rgmoddimOLD  32983  madjusmdetlem1  33105  cnre2csqlem  33188  zzsnm  33237  rrhcn  33275  qqhre  33298  oms0  33594  omsmon  33595  omssubaddlem  33596  omssubadd  33597  eulerpart  33679  fib0  33696  fib1  33697  fibp1  33698  coinflippv  33780  gsumnunsn  33850  2cycld  34427  derangenlem  34460  kur14lem2  34496  kur14lem3  34497  kur14lem5  34499  kur14lem6  34500  txsconnlem  34529  cvmliftlem4  34577  cvmliftlem5  34578  satf0sucom  34662  satf0suc  34665  satf0op  34666  fmla  34670  satffunlem2lem2  34695  satfv0fvfmla0  34702  sate0  34704  funpartfv  35221  fullfunfv  35223  neibastop2lem  35548  dffinxpf  36569  ftc1cnnc  36863  heiborlem4  36985  heiborlem6  36987  cdlemk13  40026  cdlemk14  40028  cdlemk15  40029  cdlemk21N  40047  cdlemk20  40048  cdlemk56w  40147  lcfrlem1  40716  hdmapfval  41001  evlsevl  41445  selvvvval  41459  rabdiophlem2  41842  dnnumch1  42088  aomclem6  42103  mncn0  42183  aaitgo  42206  rngunsnply  42217  cytpval  42253  dssmapntrcls  43181  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  binomcxp  43418  fvcod  44224  fvmpt2df  44275  fsumsermpt  44593  fmul01  44594  fmuldfeq  44597  fmul01lt1lem1  44598  fmul01lt1lem2  44599  lptioo2cn  44659  lptioo1cn  44660  limclner  44665  dvsinax  44927  fperdvper  44933  dvnmul  44957  dvnprodlem1  44960  dvnprodlem2  44961  dvnprodlem3  44962  itgsin0pilem1  44964  stoweidlem3  45017  stoweidlem17  45031  stoweidlem47  45061  fourierdlem42  45163  fourierdlem62  45182  fourierdlem80  45200  fourierdlem90  45210  fourierdlem92  45212  fourierdlem93  45213  fourierdlem103  45223  fourierdlem104  45224  fouriercnp  45240  sge0isum  45441  sge0seq  45460  ovnsubadd  45586  vonn0ioo  45701  vonn0icc  45702  smflimsup  45842  fcores  46075  fundcmpsurinjimaid  46377  isomushgr  46792  rhmsubclem2  47073  rhmsubcALTVlem2  47091  ply1mulgsum  47158  lineval  47162  lincvalpr  47186  lindslinindimp2lem4  47229  zlmodzxzldeplem3  47270  zlmodzxzldeplem4  47271  itcoval0mpt  47439  ackvalsuc1mpt  47451  ackval0  47453  ackval40  47466  ackval41a  47467  ackval42  47469  ackval50  47471  ehl2eudisval0  47498  2sphere0  47523  line2  47525  line2x  47527  line2y  47528  itscnhlinecirc02p  47558