Theorem fveq1i 6859

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

Syntax hints:   = wceq 1540  ‘cfv 6511

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  fveq12i  6864  fvun2  6953  fvopab3ig  6964  fvsnun1  7156  fvpr1g  7164  fvpr2g  7165  fvtp1  7169  fvtp2  7170  fvtp3  7171  fvtp1g  7172  fvtp2g  7173  fvtp3g  7174  fpropnf1  7242  fveqf1o  7277  ov  7533  ovigg  7534  ovg  7554  fvresex  7938  curry1  8083  curry2  8086  fsplitfpar  8097  suppsnop  8157  frrlem12  8276  fprlem1  8279  tfr2a  8363  rdgsucmptf  8396  rdgsucmptnf  8397  frsucmpt  8406  frsucmptn  8407  seqomlem1  8418  seqomlem3  8420  seqomlem4  8421  seqom0g  8424  seqomsuc  8425  unblem2  9240  inf3lemb  9578  inf3lemc  9579  ttrclselem1  9678  ttrclselem2  9679  trcl  9681  frrlem15  9710  r10  9721  r1sucg  9722  r1limg  9724  infxpenc2  9975  aleph0  10019  alephlim  10020  alephsuc  10021  alephfplem1  10057  alephfplem2  10058  ackbij2lem3  10193  cfsmolem  10223  infpssrlem1  10256  infpssrlem2  10257  fin23lem34  10299  fin23lem35  10300  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  isf34lem5  10331  hsmexlem7  10376  axdclem2  10473  canthp1lem2  10606  wunex2  10691  wuncval2  10700  addpiord  10837  mulpiord  10838  addpqnq  10891  mulpqnq  10894  fseq1p1m1  13559  om2uz0i  13912  om2uzrdg  13921  uzrdg0i  13924  uzrdgsuci  13925  hashkf  14297  hashgval  14298  hashinf  14300  ccat1st1st  14593  revs1  14730  cats1fv  14825  shftidt  15048  cbvsum  15661  cbvsumv  15662  fsumss  15691  isumclim3  15725  isumsup2  15812  cbvprod  15879  cbvprodv  15880  fprodss  15914  iprodclim3  15966  fprodefsum  16061  ruclem4  16202  ruclem6  16203  ruclem7  16204  sadc0  16424  sadcp1  16425  sadcaddlem  16427  sadaddlem  16436  smup0  16449  smupp1  16450  algr0  16542  algrp1  16544  ndxarg  17166  strfv2d  17171  funcoppc  17837  fthepi  17892  homadm  18002  homacd  18003  prdsidlem  18696  prdsinvlem  18981  cayleylem2  19343  symggen  19400  pmtr3ncomlem1  19403  gsumval3  19837  gsumzaddlem  19851  gsumzmhm  19867  pgpfaclem1  20013  ringidval  20092  rhmsubclem2  20595  lidlval  21120  rspval  21121  lidlnegcl  21132  lpival  21234  znf1o  21461  ply1ascl0  22139  ply1ascl1  22140  eqcoe1ply1eq  22186  evls1val  22207  evl1val  22216  mat1dimmul  22363  mdetralt  22495  mdetunilem7  22505  decpmatid  22657  pmatcollpwscmatlem1  22676  cpmidpmat  22760  chcoeffeq  22773  restcls  23068  restntr  23069  upxp  23510  cnmetdval  24658  remetdval  24677  qdensere2  24685  pcoptcl  24921  pcopt  24922  pcopt2  24923  pcorevlem  24926  isncvsngp  25049  cnncvsabsnegdemo  25065  ovolfsval  25371  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliun2  25407  ovolscalem1  25414  ovolicc2lem4  25421  mblvol  25431  ioombl1lem4  25462  uniioovol  25480  uniioombllem3  25486  0pval  25572  limccnp  25792  limccnp2  25793  dvcnvrelem2  25923  itgsubstlem  25955  ply1remlem  26070  plyrem  26213  qaa  26231  abelth  26351  efif1olem4  26454  eflog  26485  logef  26490  logeftb  26492  dvrelog  26546  dvlog  26560  cxpcn3  26658  efrlim  26879  efrlimOLD  26880  eflgam  26955  wilthlem3  26980  basellem8  26998  lgsqrlem1  27257  noetasuplem4  27648  noetainflem4  27652  precsexlem1  28109  precsexlem2  28110  precsexlem3  28111  precsexlem4  28112  precsexlem5  28113  tgcgr4  28458  krippenlem  28617  colperpexlem1  28657  opphllem3  28676  lmiisolem  28723  axlowdimlem8  28876  axlowdimlem9  28877  axlowdimlem11  28879  axlowdimlem12  28880  axlowdimlem17  28885  ushgredgedg  29156  ushgredgedgloop  29158  subgruhgredgd  29211  vtxdlfgrval  29413  vtxd0nedgb  29416  vtxdushgrfvedg  29418  vtxdginducedm1lem3  29469  finsumvtxdg2size  29478  vtxdgoddnumeven  29481  isrgr  29487  fusgrregdegfi  29497  wlk1walk  29567  wlkres  29598  wlkp1lem5  29605  wlkp1lem6  29606  wlkp1lem7  29607  wlkp1lem8  29608  clwlkcompbp  29712  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  2wlkdlem3  29857  2wlkdlem8  29863  2wlkond  29867  umgr2adedgwlk  29875  1wlkdlem4  30069  1pthond  30073  wlk2v2elem2  30085  3wlkdlem3  30090  3wlkdlem8  30096  3cycld  30107  3cyclpd  30108  eucrctshift  30172  frgrncvvdeq  30238  frgrwopreglem2  30242  ex-fpar  30391  avril1  30392  vafval  30532  smfval  30534  0vfval  30535  nmcvfval  30536  vsfval  30562  hhssabloilem  31190  pjoc2i  31367  pjcji  31613  ho0val  31679  hoival  31684  adjbdlnb  32013  nmopcoadji  32030  opsqrlem2  32070  opsqrlem5  32073  hmopidmchi  32080  hmopidmpji  32081  pjinvari  32120  pjadj2coi  32133  pj3lem1  32135  funcnvmpt  32591  pmtrprfv2  33045  cycpmco2lem7  33089  evl1fpws  33533  rgmoddimOLD  33606  rtelextdg2lem  33716  constr0  33727  constrsuc  33728  constrlim  33729  2sqr3minply  33770  cos9thpiminplylem6  33777  madjusmdetlem1  33817  cnre2csqlem  33900  zzsnm  33949  rrhcn  33987  qqhre  34010  oms0  34288  omsmon  34289  omssubaddlem  34290  omssubadd  34291  eulerpart  34373  fib0  34390  fib1  34391  fibp1  34392  coinflippv  34475  gsumnunsn  34532  2cycld  35125  derangenlem  35158  kur14lem2  35194  kur14lem3  35195  kur14lem5  35197  kur14lem6  35198  txsconnlem  35227  cvmliftlem4  35275  cvmliftlem5  35276  satf0sucom  35360  satf0suc  35363  satf0op  35364  fmla  35368  satffunlem2lem2  35393  satfv0fvfmla0  35400  sate0  35402  funpartfv  35933  fullfunfv  35935  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  neibastop2lem  36348  dffinxpf  37373  ftc1cnnc  37686  heiborlem4  37808  heiborlem6  37810  cdlemk13  40846  cdlemk14  40848  cdlemk15  40849  cdlemk21N  40867  cdlemk20  40868  cdlemk56w  40967  lcfrlem1  41536  hdmapfval  41821  deg1gprod  42128  evlsevl  42559  selvvvval  42573  rabdiophlem2  42790  dnnumch1  43033  aomclem6  43048  mncn0  43128  aaitgo  43151  rngunsnply  43158  cytpval  43191  dssmapntrcls  44117  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  binomcxp  44346  fvcod  45221  fvmpt2df  45266  fsumsermpt  45577  fmul01  45578  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  lptioo2cn  45643  lptioo1cn  45644  limclner  45649  dvsinax  45911  fperdvper  45917  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  itgsin0pilem1  45948  stoweidlem3  46001  stoweidlem17  46015  stoweidlem47  46045  fourierdlem42  46147  fourierdlem62  46166  fourierdlem80  46184  fourierdlem90  46194  fourierdlem92  46196  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fouriercnp  46224  sge0isum  46425  sge0seq  46444  ovnsubadd  46570  vonn0ioo  46685  vonn0icc  46686  smflimsup  46826  cjnpoly  46890  sinnpoly  46892  fcores  47068  fundcmpsurinjimaid  47412  isgrim  47882  gricushgr  47917  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem6  48090  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  rhmsubcALTVlem2  48270  ply1mulgsum  48379  lineval  48383  lincvalpr  48407  lindslinindimp2lem4  48450  zlmodzxzldeplem3  48491  zlmodzxzldeplem4  48492  itcoval0mpt  48655  ackvalsuc1mpt  48667  ackval0  48669  ackval40  48682  ackval41a  48683  ackval42  48685  ackval50  48687  ehl2eudisval0  48714  2sphere0  48739  line2  48741  line2x  48743  line2y  48744  itscnhlinecirc02p  48774  oppcup  49196  natoppf  49218