Theorem fveq1i 6835

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

Syntax hints:   = wceq 1542  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500

This theorem is referenced by:  fveq12i  6840  fvun2  6926  fvopab3ig  6937  funcnvmpt  6943  fvsnun1  7130  fvpr1g  7138  fvpr2g  7139  fvtp1  7143  fvtp2  7144  fvtp3  7145  fvtp1g  7146  fvtp2g  7147  fvtp3g  7148  fpropnf1  7215  fveqf1o  7250  ov  7504  ovigg  7505  ovg  7525  fvresex  7906  curry1  8047  curry2  8050  fsplitfpar  8061  suppsnop  8121  frrlem12  8240  fprlem1  8243  tfr2a  8327  rdgsucmptf  8360  rdgsucmptnf  8361  frsucmpt  8370  frsucmptn  8371  seqomlem1  8382  seqomlem3  8384  seqomlem4  8385  seqom0g  8388  seqomsuc  8389  unblem2  9196  inf3lemb  9537  inf3lemc  9538  ttrclselem1  9637  ttrclselem2  9638  trcl  9640  frrlem15  9672  r10  9683  r1sucg  9684  r1limg  9686  infxpenc2  9935  aleph0  9979  alephlim  9980  alephsuc  9981  alephfplem1  10017  alephfplem2  10018  ackbij2lem3  10153  cfsmolem  10183  infpssrlem1  10216  infpssrlem2  10217  fin23lem34  10259  fin23lem35  10260  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  isf34lem5  10291  hsmexlem7  10336  axdclem2  10433  canthp1lem2  10567  wunex2  10652  wuncval2  10661  addpiord  10798  mulpiord  10799  addpqnq  10852  mulpqnq  10855  fseq1p1m1  13543  om2uz0i  13900  om2uzrdg  13909  uzrdg0i  13912  uzrdgsuci  13913  hashkf  14285  hashgval  14286  hashinf  14288  ccat1st1st  14582  revs1  14718  cats1fv  14812  shftidt  15035  cbvsum  15648  cbvsumv  15649  fsumss  15678  isumclim3  15712  indsumhash  15783  isumsup2  15802  cbvprod  15869  cbvprodv  15870  fprodss  15904  iprodclim3  15956  fprodefsum  16051  ruclem4  16192  ruclem6  16193  ruclem7  16194  sadc0  16414  sadcp1  16415  sadcaddlem  16417  sadaddlem  16426  smup0  16439  smupp1  16440  algr0  16532  algrp1  16534  ndxarg  17157  strfv2d  17162  funcoppc  17833  fthepi  17888  homadm  17998  homacd  17999  prdsidlem  18728  prdsinvlem  19016  cayleylem2  19379  symggen  19436  pmtr3ncomlem1  19439  gsumval3  19873  gsumzaddlem  19887  gsumzmhm  19903  pgpfaclem1  20049  ringidval  20155  rhmsubclem2  20654  lidlval  21200  rspval  21201  lidlnegcl  21212  lpival  21314  znf1o  21541  ply1ascl0  22228  ply1ascl1  22229  eqcoe1ply1eq  22274  evls1val  22295  evl1val  22304  mat1dimmul  22451  mdetralt  22583  mdetunilem7  22593  decpmatid  22745  pmatcollpwscmatlem1  22764  cpmidpmat  22848  chcoeffeq  22861  restcls  23156  restntr  23157  upxp  23598  cnmetdval  24745  remetdval  24764  qdensere2  24772  pcoptcl  24998  pcopt  24999  pcopt2  25000  pcorevlem  25003  isncvsngp  25126  cnncvsabsnegdemo  25142  ovolfsval  25447  ovollb2lem  25465  ovolunlem1a  25473  ovoliunlem1  25479  ovoliun2  25483  ovolscalem1  25490  ovolicc2lem4  25497  mblvol  25507  ioombl1lem4  25538  uniioovol  25556  uniioombllem3  25562  0pval  25648  limccnp  25868  limccnp2  25869  dvcnvrelem2  25995  itgsubstlem  26025  ply1remlem  26140  plyrem  26282  qaa  26300  abelth  26419  efif1olem4  26522  eflog  26553  logef  26558  logeftb  26560  dvrelog  26614  dvlog  26628  cxpcn3  26725  efrlim  26946  efrlimOLD  26947  eflgam  27022  wilthlem3  27047  basellem8  27065  lgsqrlem1  27323  noetasuplem4  27714  noetainflem4  27718  precsexlem1  28213  precsexlem2  28214  precsexlem3  28215  precsexlem4  28216  precsexlem5  28217  tgcgr4  28613  krippenlem  28772  colperpexlem1  28812  opphllem3  28831  lmiisolem  28878  axlowdimlem8  29032  axlowdimlem9  29033  axlowdimlem11  29035  axlowdimlem12  29036  axlowdimlem17  29041  ushgredgedg  29312  ushgredgedgloop  29314  subgruhgredgd  29367  vtxdlfgrval  29569  vtxd0nedgb  29572  vtxdushgrfvedg  29574  vtxdginducedm1lem3  29625  finsumvtxdg2size  29634  vtxdgoddnumeven  29637  isrgr  29643  fusgrregdegfi  29653  wlk1walk  29722  wlkres  29752  wlkp1lem5  29759  wlkp1lem6  29760  wlkp1lem7  29761  wlkp1lem8  29762  clwlkcompbp  29865  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem6  29898  2wlkdlem3  30010  2wlkdlem8  30016  2wlkond  30020  umgr2adedgwlk  30028  1wlkdlem4  30225  1pthond  30229  wlk2v2elem2  30241  3wlkdlem3  30246  3wlkdlem8  30252  3cycld  30263  3cyclpd  30264  eucrctshift  30328  frgrncvvdeq  30394  frgrwopreglem2  30398  ex-fpar  30547  avril1  30548  vafval  30689  smfval  30691  0vfval  30692  nmcvfval  30693  vsfval  30719  hhssabloilem  31347  pjoc2i  31524  pjcji  31770  ho0val  31836  hoival  31841  adjbdlnb  32170  nmopcoadji  32187  opsqrlem2  32227  opsqrlem5  32230  hmopidmchi  32237  hmopidmpji  32238  pjinvari  32277  pjadj2coi  32290  pj3lem1  32292  pmtrprfv2  33164  cycpmco2lem7  33208  evl1fpws  33639  mplmulmvr  33698  evlextv  33701  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  esplyindfv  33735  esplyfvn  33736  vietalem  33738  rgmoddimOLD  33770  rtelextdg2lem  33886  constr0  33897  constrsuc  33898  constrlim  33899  2sqr3minply  33940  cos9thpiminplylem6  33947  madjusmdetlem1  33987  cnre2csqlem  34070  zzsnm  34119  rrhcn  34157  qqhre  34180  oms0  34457  omsmon  34458  omssubaddlem  34459  omssubadd  34460  eulerpart  34542  fib0  34559  fib1  34560  fibp1  34561  coinflippv  34644  gsumnunsn  34701  2cycld  35336  derangenlem  35369  kur14lem2  35405  kur14lem3  35406  kur14lem5  35408  kur14lem6  35409  txsconnlem  35438  cvmliftlem4  35486  cvmliftlem5  35487  satf0sucom  35571  satf0suc  35574  satf0op  35575  fmla  35579  satffunlem2lem2  35604  satfv0fvfmla0  35611  sate0  35613  funpartfv  36143  fullfunfv  36145  sumeq2si  36400  prodeq2si  36402  cbvprodvw2  36445  neibastop2lem  36558  dffinxpf  37715  ftc1cnnc  38027  heiborlem4  38149  heiborlem6  38151  cdlemk13  41312  cdlemk14  41314  cdlemk15  41315  cdlemk21N  41333  cdlemk20  41334  cdlemk56w  41433  lcfrlem1  42002  hdmapfval  42287  deg1gprod  42593  evlsevl  43021  selvvvval  43032  rabdiophlem2  43248  dnnumch1  43490  aomclem6  43505  mncn0  43585  aaitgo  43608  rngunsnply  43615  cytpval  43648  dssmapntrcls  44573  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  binomcxp  44802  fvcod  45674  fvmpt2df  45719  fsumsermpt  46027  fmul01  46028  fmuldfeq  46031  fmul01lt1lem1  46032  fmul01lt1lem2  46033  lptioo2cn  46091  lptioo1cn  46092  limclner  46097  dvsinax  46359  fperdvper  46365  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  itgsin0pilem1  46396  stoweidlem3  46449  stoweidlem17  46463  stoweidlem47  46493  fourierdlem42  46595  fourierdlem62  46614  fourierdlem80  46632  fourierdlem90  46642  fourierdlem92  46644  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  fouriercnp  46672  sge0isum  46873  sge0seq  46892  ovnsubadd  47018  vonn0ioo  47133  vonn0icc  47134  smflimsup  47274  cjnpoly  47349  sinnpoly  47351  fcores  47527  fundcmpsurinjimaid  47883  isgrim  48370  gricushgr  48405  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem6  48588  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592  rhmsubcALTVlem2  48770  ply1mulgsum  48878  lineval  48882  lincvalpr  48906  lindslinindimp2lem4  48949  zlmodzxzldeplem3  48990  zlmodzxzldeplem4  48991  itcoval0mpt  49154  ackvalsuc1mpt  49166  ackval0  49168  ackval40  49181  ackval41a  49182  ackval42  49184  ackval50  49186  ehl2eudisval0  49213  2sphere0  49238  line2  49240  line2x  49242  line2y  49243  itscnhlinecirc02p  49273  oppcup  49694  natoppf  49716