Theorem fveq1i 6884

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

This proof depends on syntax axioms:   = wceq 1570  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545

This theorem is used by:  fveq12i  6889  fvun2  6975  fvcod  6982  fvopab3ig  6987  funcnvmpt  6993  fvsnun1  7185  fvpr1g  7193  fvpr2g  7194  fvtp1  7198  fvtp2  7199  fvtp3  7200  fvtp1g  7201  fvtp2g  7202  fvtp3g  7203  fpropnf1  7269  fveqf1o  7308  ov  7562  ovigg  7563  ovg  7583  mpt3fvd  7686  fvresex  7970  curry1  8113  curry2  8116  fsplitfpar  8127  suppsnop  8188  frrlem12  8308  fprlem1  8311  tfr2a  8396  rdgsucmptf  8429  rdgsucmptnf  8430  frsucmpt  8439  frsucmptn  8440  seqomlem1  8453  seqomlem3  8455  seqomlem4  8456  seqom0g  8459  seqomsuc  8460  unblem2  9278  inf3lemb  9619  inf3lemc  9620  ttrclselem1  9719  ttrclselem2  9720  trcl  9722  frrlem15  9754  r10  9768  r1sucg  9769  r1limg  9771  infxpenc2  10094  aleph0  10138  alephlim  10139  alephsuc  10140  alephfplem1  10176  alephfplem2  10177  ackbij2lem3  10311  cfsmolem  10341  infpssrlem1  10374  infpssrlem2  10375  fin23lem34  10417  fin23lem35  10418  isf32lem6  10429  isf32lem7  10430  isf32lem8  10431  isf34lem5  10449  hsmexlem7  10494  axdclem2  10591  canthp1lem2  10731  wunex2  10816  wuncval2  10825  addpiord  10962  mulpiord  10963  addpqnq  11016  mulpqnq  11019  fseq1p1m1  13725  om2uz0i  14083  om2uzrdg  14092  uzrdg0i  14095  uzrdgsuci  14096  hashkf  14469  hashgval  14470  hashinf  14472  ccat1st1st  14769  revs1  14907  cats1fv  15003  shftidt  15228  cbvsum  15855  cbvsumv  15856  fsumss  15884  isumclim3  15918  indsumhash  15989  isumsup2  16008  cbvprod  16075  cbvprodv  16076  fprodss  16108  iprodclim3  16160  fprodefsum  16254  ruclem4  16395  ruclem6  16396  ruclem7  16397  sadc0  16617  sadcp1  16618  sadcaddlem  16620  sadaddlem  16629  smup0  16642  smupp1  16643  algr0  16740  algrp1  16742  ndxarg  17367  strfv2d  17372  funcoppc  18043  fthepi  18098  homadm  18208  homacd  18209  prdsidlem  18956  prdsinvlem  19252  cayleylem2  19620  symggen  19677  pmtr3ncomlem1  19680  gsumval3  20114  gsumzaddlem  20128  gsumzmhm  20144  pgpfaclem1  20290  ringidval  20402  rhmsubclem2  20931  lidlval  21481  rspval  21482  lidlnegcl  21494  rspvalint  21516  lpival  21641  znf1o  21850  evlsevl  22434  selvvvval  22444  ply1ascl0  22565  ply1ascl1  22566  eqcoe1ply1eq  22610  evls1val  22631  evl1val  22640  mat1dimmul  22784  mdetralt  22916  mdetunilem7  22926  decpmatid  23081  pmatcollpwscmatlem1  23100  cpmidpmat  23184  chcoeffeq  23197  restcls  23492  restntr  23493  upxp  23935  cnmetdval  25082  remetdval  25101  qdensere2  25109  pcoptcl  25335  pcopt  25336  pcopt2  25337  pcorevlem  25340  isncvsngp  25463  cnncvsabsnegdemo  25479  ovolfsval  25784  ovollb2lem  25802  ovolunlem1a  25810  ovoliunlem1  25816  ovoliun2  25820  ovolscalem1  25827  ovolicc2lem4  25834  mblvol  25844  ioombl1lem4  25875  uniioovol  25893  uniioombllem3  25899  0pval  25985  limccnp  26204  limccnp2  26205  dvcnvrelem2  26331  itgsubstlem  26361  ply1remlem  26476  idpfv  26521  plyrem  26619  qaa  26640  abelth  26761  efif1olem4  26866  eflog  26897  logef  26902  logeftb  26904  dvrelog  26958  dvlog  26972  cxpcn3  27069  efrlim  27290  eflgam  27365  wilthlem3  27390  basellem8  27408  lgsqrlem1  27666  noetasuplem4  28086  noetainflem4  28090  precsexlem1  28586  precsexlem2  28587  precsexlem3  28588  precsexlem4  28589  precsexlem5  28590  tgcgr4  28987  krippenlem  29155  colperpexlem1  29199  opphllem3  29218  lmiisolem  29294  axlowdimlem8  29520  axlowdimlem9  29521  axlowdimlem11  29523  axlowdimlem12  29524  axlowdimlem17  29529  ushgredgedg  29803  ushgredgedgloop  29805  subgruhgredgd  29858  vtxdlfgrval  30059  vtxd0nedgb  30062  vtxdushgrfvedg  30064  vtxdginducedm1lem3  30115  finsumvtxdg2size  30124  vtxdgoddnumeven  30127  isrgr  30133  fusgrregdegfi  30143  wlk1walk  30212  wlkres  30242  wlkp1lem5  30249  wlkp1lem6  30250  wlkp1lem7  30251  wlkp1lem8  30252  clwlkcompbp  30362  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  crctcshwlkn0lem6  30397  2wlkdlem3  30509  2wlkdlem8  30515  2wlkond  30519  umgr2adedgwlk  30527  1wlkdlem4  30724  1pthond  30728  2cycld  30738  wlk2v2elem2  30750  3wlkdlem3  30755  3wlkdlem8  30761  3cycld  30772  3cyclpd  30773  eucrctshift  30837  frgrncvvdeq  30903  frgrwopreglem2  30907  ex-fpar  31056  avril1  31057  vafval  31198  smfval  31200  0vfval  31201  nmcvfval  31202  vsfval  31228  hhssabloilem  31856  pjoc2i  32033  pjcji  32279  ho0val  32345  hoival  32350  adjbdlnb  32679  nmopcoadji  32696  opsqrlem2  32736  opsqrlem5  32739  hmopidmchi  32746  hmopidmpji  32747  pjinvari  32786  pjadj2coi  32799  pj3lem1  32801  pmtrprfv2  33642  cycpmco2lem7  33686  evl1fpws  34089  mplmulmvr  34164  evlextv  34167  esplyfval1  34198  esplyfvaln  34199  esplyind  34200  esplyindfv  34201  esplyfvn  34202  vietalem  34204  rtelextdg2lem  34351  constr0  34362  constrsuc  34363  constrlim  34364  2sqr3minply  34405  cos9thpiminplylem6  34412  madjusmdetlem1  34452  cnre2csqlem  34535  zzsnm  34584  rrhcn  34622  qqhre  34645  oms0  34922  omsmon  34923  omssubaddlem  34924  omssubadd  34925  eulerpart  35007  fib0  35024  fib1  35025  fibp1  35026  coinflippv  35109  gsumnunsn  35166  derangenlem  35915  kur14lem2  35951  kur14lem3  35952  kur14lem5  35954  kur14lem6  35955  txsconnlem  35984  cvmliftlem4  36032  cvmliftlem5  36033  satf0sucom  36117  satf0suc  36120  satf0op  36121  fmla  36125  satffunlem2lem2  36150  satfv0fvfmla0  36157  sate0  36159  funpartfv  36689  fullfunfv  36691  sumeq2si  36971  prodeq2si  36973  cbvprodvw2  37016  neibastop2lem  37128  dffinxpf  38288  ftc1cnnc  38590  heiborlem4  38728  heiborlem6  38730  cdlemk13  41889  cdlemk14  41891  cdlemk15  41892  cdlemk21N  41910  cdlemk20  41911  cdlemk56w  42010  lcfrlem1  42579  hdmapfval  42864  deg1gprod  43170  rabdiophlem2  43788  dnnumch1  44030  aomclem6  44045  mncn0  44125  aaitgo  44148  rngunsnply  44155  cytpval  44188  dssmapntrcls  45113  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  binomcxp  45326  fvmpt2df  46253  fsumsermpt  46560  fmul01  46561  fmuldfeq  46564  fmul01lt1lem1  46565  fmul01lt1lem2  46566  lptioo2cn  46624  lptioo1cn  46625  limclner  46630  dvsinax  46892  fperdvper  46898  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  dvnprodlem3  46927  itgsin0pilem1  46929  stoweidlem3  46982  stoweidlem17  46996  stoweidlem47  47026  fourierdlem42  47128  fourierdlem62  47147  fourierdlem80  47165  fourierdlem90  47175  fourierdlem92  47177  fourierdlem93  47178  fourierdlem103  47188  fourierdlem104  47189  fouriercnp  47205  sge0isum  47406  sge0seq  47425  ovnsubadd  47551  vonn0ioo  47666  vonn0icc  47667  smflimsup  47807  cjnpoly  47908  sinnpoly  47910  fcores  48106  fundcmpsurinjimaid  48462  isgrim  48949  gricushgr  48984  gpgprismgr4cycllem3  49164  gpgprismgr4cycllem6  49167  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  rhmsubcALTVlem2  49348  ply1mulgsum  49471  lineval  49475  lincvalpr  49499  lindslinindimp2lem4  49542  zlmodzxzldeplem3  49583  zlmodzxzldeplem4  49584  itcoval0mpt  49747  ackvalsuc1mpt  49759  ackval0  49761  ackval40  49774  ackval41a  49775  ackval42  49777  ackval50  49779  ehl2eudisval0  49806  2sphere0  49831  line2  49833  line2x  49835  line2y  49836  itscnhlinecirc02p  49866  oppcup  50284  natoppf  50306