Theorem fveq1i 6917

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574

This theorem is used by:  fveq12i  6922  fvun2  7008  fvcod  7015  fvopab3ig  7020  funcnvmpt  7026  fvsnun1  7218  fvpr1g  7226  fvpr2g  7227  fvtp1  7231  fvtp2  7232  fvtp3  7233  fvtp1g  7234  fvtp2g  7235  fvtp3g  7236  fpropnf1  7302  fveqf1o  7341  ov  7596  ovigg  7597  ovg  7617  mpt3fvd  7720  fvresex  8006  curry1  8152  curry2  8155  fsplitfpar  8166  suppsnop  8233  frrlem12  8353  fprlem1  8356  tfr2a  8441  rdgsucmptf  8474  rdgsucmptnf  8475  frsucmpt  8484  frsucmptn  8485  seqomlem1  8498  seqomlem3  8500  seqomlem4  8501  seqom0g  8504  seqomsuc  8505  unblem2  9323  inf3lemb  9663  inf3lemc  9664  ttrclselem1  9763  ttrclselem2  9764  trcl  9766  frrlem15  9798  r10  9812  r1sucg  9813  r1limg  9815  infxpenc2  10140  aleph0  10184  alephlim  10185  alephsuc  10186  alephfplem1  10222  alephfplem2  10223  ackbij2lem3  10357  cfsmolem  10387  infpssrlem1  10420  infpssrlem2  10421  fin23lem34  10463  fin23lem35  10464  isf32lem6  10475  isf32lem7  10476  isf32lem8  10477  isf34lem5  10495  hsmexlem7  10540  axdclem2  10637  canthp1lem2  10777  wunex2  10862  wuncval2  10871  addpiord  11008  mulpiord  11009  addpqnq  11062  mulpqnq  11065  fseq1p1m1  13772  om2uz0i  14130  om2uzrdg  14139  uzrdg0i  14142  uzrdgsuci  14143  hashkf  14517  hashgval  14518  hashinf  14520  ccat1st1st  14818  revs1  14956  cats1fv  15052  shftidt  15278  cbvsum  15906  cbvsumv  15907  fsumss  15935  isumclim3  15969  indsumhash  16040  isumsup2  16059  cbvprod  16126  cbvprodv  16127  fprodss  16159  iprodclim3  16211  fprodefsum  16305  ruclem4  16446  ruclem6  16447  ruclem7  16448  sadc0  16668  sadcp1  16669  sadcaddlem  16671  sadaddlem  16680  smup0  16693  smupp1  16694  algr0  16791  algrp1  16793  ndxarg  17418  strfv2d  17423  funcoppc  18100  fthepi  18155  homadm  18265  homacd  18266  prdsidlem  19013  prdsinvlem  19309  cayleylem2  19678  symggen  19735  pmtr3ncomlem1  19738  gsumval3  20172  gsumzaddlem  20186  gsumzmhm  20202  pgpfaclem1  20348  ringidval  20460  rhmsubclem2  20989  lidlval  21539  rspval  21540  lidlnegcl  21552  rspvalint  21574  lpival  21699  znf1o  21912  evlsevl  22496  selvvvval  22506  ply1ascl0  22627  ply1ascl1  22628  eqcoe1ply1eq  22672  evls1val  22693  evl1val  22702  mat1dimmul  22846  mdetralt  22978  mdetunilem7  22988  decpmatid  23143  pmatcollpwscmatlem1  23162  cpmidpmat  23246  chcoeffeq  23259  restcls  23554  restntr  23555  upxp  23997  cnmetdval  25144  remetdval  25163  qdensere2  25171  pcoptcl  25397  pcopt  25398  pcopt2  25399  pcorevlem  25402  isncvsngp  25525  cnncvsabsnegdemo  25541  ovolfsval  25846  ovollb2lem  25864  ovolunlem1a  25872  ovoliunlem1  25878  ovoliun2  25882  ovolscalem1  25889  ovolicc2lem4  25896  mblvol  25906  ioombl1lem4  25937  uniioovol  25955  uniioombllem3  25961  0pval  26047  limccnp  26266  limccnp2  26267  dvcnvrelem2  26393  itgsubstlem  26423  ply1remlem  26538  idpfv  26583  plyrem  26681  rngunsnply  26693  abelth  26825  efif1olem4  26930  eflog  26961  logef  26966  logeftb  26968  dvrelog  27022  dvlog  27036  cxpcn3  27133  efrlim  27354  eflgam  27429  wilthlem3  27454  basellem8  27472  lgsqrlem1  27730  noetasuplem4  28150  noetainflem4  28154  precsexlem1  28650  precsexlem2  28651  precsexlem3  28652  precsexlem4  28653  precsexlem5  28654  tgcgr4  29051  krippenlem  29219  colperpexlem1  29263  opphllem3  29282  lmiisolem  29358  axlowdimlem8  29584  axlowdimlem9  29585  axlowdimlem11  29587  axlowdimlem12  29588  axlowdimlem17  29593  ushgredgedg  29867  ushgredgedgloop  29869  subgruhgredgd  29922  vtxdlfgrval  30123  vtxd0nedgb  30126  vtxdushgrfvedg  30128  vtxdginducedm1lem3  30179  finsumvtxdg2size  30188  vtxdgoddnumeven  30191  isrgr  30197  fusgrregdegfi  30207  wlk1walk  30276  wlkres  30306  wlkp1lem5  30313  wlkp1lem6  30314  wlkp1lem7  30315  wlkp1lem8  30316  clwlkcompbp  30426  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  2wlkdlem3  30573  2wlkdlem8  30579  2wlkond  30583  umgr2adedgwlk  30591  1wlkdlem4  30788  1pthond  30792  2cycld  30802  wlk2v2elem2  30814  3wlkdlem3  30819  3wlkdlem8  30825  3cycld  30836  3cyclpd  30837  eucrctshift  30901  frgrncvvdeq  30967  frgrwopreglem2  30971  ex-fpar  31120  avril1  31121  vafval  31262  smfval  31264  0vfval  31265  nmcvfval  31266  vsfval  31292  hhssabloilem  31920  pjoc2i  32097  pjcji  32343  ho0val  32409  hoival  32414  adjbdlnb  32743  nmopcoadji  32760  opsqrlem2  32800  opsqrlem5  32803  hmopidmchi  32810  hmopidmpji  32811  pjinvari  32850  pjadj2coi  32863  pj3lem1  32865  pmtrprfv2  33748  cycpmco2lem7  33792  isedom  33953  evl1fpws  34199  evls1degle1  34239  rngunsnply1chr2lem3  34252  mplmulmvr  34282  evlextv  34285  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  esplyindfv  34319  esplyfvn  34320  vietalem  34322  rtelextdg2lem  34469  constr0  34480  constrsuc  34481  constrlim  34482  2sqr3minply  34523  cos9thpiminplylem6  34530  madjusmdetlem1  34570  cnre2csqlem  34653  zzsnm  34702  rrhcn  34740  qqhre  34763  oms0  35040  omsmon  35041  omssubaddlem  35042  omssubadd  35043  eulerpart  35125  fib0  35142  fib1  35143  fibp1  35144  coinflippv  35227  gsumnunsn  35284  fwfffunres  35829  derangenlem  36144  kur14lem2  36180  kur14lem3  36181  kur14lem5  36183  kur14lem6  36184  txsconnlem  36213  cvmliftlem4  36261  cvmliftlem5  36262  satf0sucom  36346  satf0suc  36349  satf0op  36350  fmla  36354  satffunlem2lem2  36379  satfv0fvfmla0  36386  sate0  36388  funpartfv  36924  fullfunfv  36926  sumeq2si  37206  prodeq2si  37208  cbvprodvw2  37251  neibastop2lem  37363  dffinxpf  38576  ftc1cnnc  38878  heiborlem4  39014  heiborlem6  39016  cdlemk13  42175  cdlemk14  42177  cdlemk15  42178  cdlemk21N  42196  cdlemk20  42197  cdlemk56w  42296  lcfrlem1  42865  hdmapfval  43150  deg1gprod  43456  rabdiophlem2  44075  dnnumch1  44317  aomclem6  44327  mncn0  44406  aaitgo  44429  cytpval  44465  dssmapntrcls  45389  binomcxplemdvsum  45600  binomcxplemnotnn0  45601  binomcxp  45602  fvmpt2df  46557  fsumsermpt  46864  fmul01  46865  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  lptioo2cn  46928  lptioo1cn  46929  limclner  46934  dvsinax  47196  fperdvper  47202  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  dvnprodlem3  47231  itgsin0pilem1  47233  stoweidlem3  47286  stoweidlem17  47300  stoweidlem47  47330  fourierdlem42  47432  fourierdlem62  47451  fourierdlem80  47469  fourierdlem90  47479  fourierdlem92  47481  fourierdlem93  47482  fourierdlem103  47492  fourierdlem104  47493  fouriercnp  47509  sge0isum  47710  sge0seq  47729  ovnsubadd  47855  vonn0ioo  47970  vonn0icc  47971  smflimsup  48111  cjnpoly  48212  sinnpoly  48214  fcores  48410  fundcmpsurinjimaid  48766  isgrim  49253  gricushgr  49288  gpgprismgr4cycllem3  49468  gpgprismgr4cycllem6  49471  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  rhmsubcALTVlem2  49652  ply1mulgsum  49833  lineval  49837  lincvalpr  49861  lindslinindimp2lem4  49904  zlmodzxzldeplem3  49945  zlmodzxzldeplem4  49946  itcoval0mpt  50109  ackvalsuc1mpt  50121  ackval0  50123  ackval40  50136  ackval41a  50137  ackval42  50139  ackval50  50141  ehl2eudisval0  50169  2sphere0  50193  line2  50195  line2x  50197  line2y  50198  oppcup  50654  natoppf  50682  par2diag  51111  fuconuniqvalslem  51114