Theorem fveq1i 6902

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

Syntax hints:   = wceq 1534  ‘cfv 6554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562

This theorem is referenced by:  fveq12i  6907  fvun2  6994  fvopab3ig  7005  fvsnun1  7196  fvpr1g  7204  fvpr2g  7205  fvpr2gOLD  7206  fvpr1OLD  7208  fvpr2OLD  7210  fvtp1  7212  fvtp2  7213  fvtp3  7214  fvtp1g  7215  fvtp2g  7216  fvtp3g  7217  fpropnf1  7282  fveqf1o  7316  ov  7570  ovigg  7571  ovg  7591  fvresex  7973  curry1  8118  curry2  8121  fsplitfpar  8132  suppsnop  8192  frrlem12  8312  fprlem1  8315  wfrlem5OLD  8343  tfr2a  8425  rdgsucmptf  8458  rdgsucmptnf  8459  frsucmpt  8468  frsucmptn  8469  seqomlem1  8480  seqomlem3  8482  seqomlem4  8483  seqom0g  8486  seqomsuc  8487  unblem2  9330  inf3lemb  9668  inf3lemc  9669  ttrclselem1  9768  ttrclselem2  9769  trcl  9771  frrlem15  9800  r10  9811  r1sucg  9812  r1limg  9814  infxpenc2  10065  aleph0  10109  alephlim  10110  alephsuc  10111  alephfplem1  10147  alephfplem2  10148  ackbij2lem3  10284  cfsmolem  10313  infpssrlem1  10346  infpssrlem2  10347  fin23lem34  10389  fin23lem35  10390  isf32lem6  10401  isf32lem7  10402  isf32lem8  10403  isf34lem5  10421  hsmexlem7  10466  axdclem2  10563  canthp1lem2  10696  wunex2  10781  wuncval2  10790  addpiord  10927  mulpiord  10928  addpqnq  10981  mulpqnq  10984  fseq1p1m1  13629  om2uz0i  13967  om2uzrdg  13976  uzrdg0i  13979  uzrdgsuci  13980  hashkf  14349  hashgval  14350  hashinf  14352  ccat1st1st  14636  revs1  14773  cats1fv  14868  shftidt  15087  cbvsum  15699  fsumss  15729  isumclim3  15763  isumsup2  15850  cbvprod  15917  fprodss  15950  iprodclim3  16002  fprodefsum  16097  ruclem4  16236  ruclem6  16237  ruclem7  16238  sadc0  16454  sadcp1  16455  sadcaddlem  16457  sadaddlem  16466  smup0  16479  smupp1  16480  algr0  16573  algrp1  16575  ndxarg  17198  strfv2d  17204  funcoppc  17894  fthepi  17950  homadm  18062  homacd  18063  prdsidlem  18759  prdsinvlem  19043  cayleylem2  19411  symggen  19468  pmtr3ncomlem1  19471  gsumval3  19905  gsumzaddlem  19919  gsumzmhm  19935  pgpfaclem1  20081  ringidval  20166  rhmsubclem2  20664  lidlval  21199  rspval  21200  lidlnegcl  21211  lpival  21313  znf1o  21549  ply1ascl0  22244  ply1ascl1  22245  eqcoe1ply1eq  22290  evls1val  22311  evl1val  22320  mat1dimmul  22469  mdetralt  22601  mdetunilem7  22611  decpmatid  22763  pmatcollpwscmatlem1  22782  cpmidpmat  22866  chcoeffeq  22879  restcls  23176  restntr  23177  upxp  23618  cnmetdval  24778  remetdval  24796  qdensere2  24804  pcoptcl  25039  pcopt  25040  pcopt2  25041  pcorevlem  25044  isncvsngp  25168  cnncvsabsnegdemo  25184  ovolfsval  25490  ovollb2lem  25508  ovolunlem1a  25516  ovoliunlem1  25522  ovoliun2  25526  ovolscalem1  25533  ovolicc2lem4  25540  mblvol  25550  ioombl1lem4  25581  uniioovol  25599  uniioombllem3  25605  0pval  25691  limccnp  25911  limccnp2  25912  dvcnvrelem2  26042  itgsubstlem  26074  ply1remlem  26192  plyrem  26333  qaa  26351  abelth  26471  efif1olem4  26572  eflog  26603  logef  26608  logeftb  26610  dvrelog  26664  dvlog  26678  cxpcn3  26776  efrlim  26997  efrlimOLD  26998  eflgam  27073  wilthlem3  27098  basellem8  27116  lgsqrlem1  27375  noetasuplem4  27766  noetainflem4  27770  precsexlem1  28206  precsexlem2  28207  precsexlem3  28208  precsexlem4  28209  precsexlem5  28210  tgcgr4  28458  krippenlem  28617  colperpexlem1  28657  opphllem3  28676  lmiisolem  28723  axlowdimlem8  28883  axlowdimlem9  28884  axlowdimlem11  28886  axlowdimlem12  28887  axlowdimlem17  28892  ushgredgedg  29165  ushgredgedgloop  29167  subgruhgredgd  29220  vtxdlfgrval  29422  vtxd0nedgb  29425  vtxdushgrfvedg  29427  vtxdginducedm1lem3  29478  finsumvtxdg2size  29487  vtxdgoddnumeven  29490  isrgr  29496  fusgrregdegfi  29506  wlk1walk  29576  wlkres  29607  wlkp1lem5  29614  wlkp1lem6  29615  wlkp1lem7  29616  wlkp1lem8  29617  clwlkcompbp  29719  crctcshwlkn0lem4  29747  crctcshwlkn0lem5  29748  crctcshwlkn0lem6  29749  2wlkdlem3  29861  2wlkdlem8  29867  2wlkond  29871  umgr2adedgwlk  29879  1wlkdlem4  30073  1pthond  30077  wlk2v2elem2  30089  3wlkdlem3  30094  3wlkdlem8  30100  3cycld  30111  3cyclpd  30112  eucrctshift  30176  frgrncvvdeq  30242  frgrwopreglem2  30246  ex-fpar  30395  avril1  30396  vafval  30536  smfval  30538  0vfval  30539  nmcvfval  30540  vsfval  30566  hhssabloilem  31194  pjoc2i  31371  pjcji  31617  ho0val  31683  hoival  31688  adjbdlnb  32017  nmopcoadji  32034  opsqrlem2  32074  opsqrlem5  32077  hmopidmchi  32084  hmopidmpji  32085  pjinvari  32124  pjadj2coi  32137  pj3lem1  32139  funcnvmpt  32584  pmtrprfv2  32966  cycpmco2lem7  33010  evl1fpws  33437  rgmoddimOLD  33505  constr0  33595  constrsuc  33596  constrlim  33597  rtelextdg2lem  33604  2sqr3minply  33607  madjusmdetlem1  33642  cnre2csqlem  33725  zzsnm  33774  rrhcn  33812  qqhre  33835  oms0  34131  omsmon  34132  omssubaddlem  34133  omssubadd  34134  eulerpart  34216  fib0  34233  fib1  34234  fibp1  34235  coinflippv  34317  gsumnunsn  34387  2cycld  34966  derangenlem  34999  kur14lem2  35035  kur14lem3  35036  kur14lem5  35038  kur14lem6  35039  txsconnlem  35068  cvmliftlem4  35116  cvmliftlem5  35117  satf0sucom  35201  satf0suc  35204  satf0op  35205  fmla  35209  satffunlem2lem2  35234  satfv0fvfmla0  35241  sate0  35243  funpartfv  35769  fullfunfv  35771  neibastop2lem  36072  dffinxpf  37092  ftc1cnnc  37393  heiborlem4  37515  heiborlem6  37517  cdlemk13  40551  cdlemk14  40553  cdlemk15  40554  cdlemk21N  40572  cdlemk20  40573  cdlemk56w  40672  lcfrlem1  41241  hdmapfval  41526  deg1gprod  41838  evlsevl  42043  selvvvval  42057  rabdiophlem2  42459  dnnumch1  42705  aomclem6  42720  mncn0  42800  aaitgo  42823  rngunsnply  42834  cytpval  42867  dssmapntrcls  43795  binomcxplemdvsum  44029  binomcxplemnotnn0  44030  binomcxp  44031  fvcod  44834  fvmpt2df  44882  fsumsermpt  45200  fmul01  45201  fmuldfeq  45204  fmul01lt1lem1  45205  fmul01lt1lem2  45206  lptioo2cn  45266  lptioo1cn  45267  limclner  45272  dvsinax  45534  fperdvper  45540  dvnmul  45564  dvnprodlem1  45567  dvnprodlem2  45568  dvnprodlem3  45569  itgsin0pilem1  45571  stoweidlem3  45624  stoweidlem17  45638  stoweidlem47  45668  fourierdlem42  45770  fourierdlem62  45789  fourierdlem80  45807  fourierdlem90  45817  fourierdlem92  45819  fourierdlem93  45820  fourierdlem103  45830  fourierdlem104  45831  fouriercnp  45847  sge0isum  46048  sge0seq  46067  ovnsubadd  46193  vonn0ioo  46308  vonn0icc  46309  smflimsup  46449  fcores  46682  fundcmpsurinjimaid  46983  isgrim  47447  gricushgr  47465  rhmsubcALTVlem2  47659  ply1mulgsum  47773  lineval  47777  lincvalpr  47801  lindslinindimp2lem4  47844  zlmodzxzldeplem3  47885  zlmodzxzldeplem4  47886  itcoval0mpt  48054  ackvalsuc1mpt  48066  ackval0  48068  ackval40  48081  ackval41a  48082  ackval42  48084  ackval50  48086  ehl2eudisval0  48113  2sphere0  48138  line2  48140  line2x  48142  line2y  48143  itscnhlinecirc02p  48173