Theorem fveq1i 6828

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

Syntax hints:   = wceq 1547  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493

This theorem is referenced by:  fveq12i  6833  fvun2  6919  fvcod  6926  fvopab3ig  6931  funcnvmpt  6937  fvsnun1  7126  fvpr1g  7134  fvpr2g  7135  fvtp1  7139  fvtp2  7140  fvtp3  7141  fvtp1g  7142  fvtp2g  7143  fvtp3g  7144  fpropnf1  7211  fveqf1o  7246  ov  7500  ovigg  7501  ovg  7521  fvresex  7902  curry1  8043  curry2  8046  fsplitfpar  8057  suppsnop  8118  frrlem12  8237  fprlem1  8240  tfr2a  8324  rdgsucmptf  8357  rdgsucmptnf  8358  frsucmpt  8367  frsucmptn  8368  seqomlem1  8379  seqomlem3  8381  seqomlem4  8382  seqom0g  8385  seqomsuc  8386  unblem2  9193  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  20658  lidlval  21203  rspval  21204  lidlnegcl  21215  lpival  21317  znf1o  21526  evlsevl  22108  selvvvval  22118  ply1ascl0  22239  ply1ascl1  22240  eqcoe1ply1eq  22285  evls1val  22306  evl1val  22315  mat1dimmul  22459  mdetralt  22591  mdetunilem7  22601  decpmatid  22753  pmatcollpwscmatlem1  22772  cpmidpmat  22856  chcoeffeq  22869  restcls  23164  restntr  23165  upxp  23606  cnmetdval  24753  remetdval  24772  qdensere2  24780  pcoptcl  25006  pcopt  25007  pcopt2  25008  pcorevlem  25011  isncvsngp  25134  cnncvsabsnegdemo  25150  ovolfsval  25455  ovollb2lem  25473  ovolunlem1a  25481  ovoliunlem1  25487  ovoliun2  25491  ovolscalem1  25498  ovolicc2lem4  25505  mblvol  25515  ioombl1lem4  25546  uniioovol  25564  uniioombllem3  25570  0pval  25656  limccnp  25876  limccnp2  25877  dvcnvrelem2  26003  itgsubstlem  26033  ply1remlem  26148  plyrem  26289  qaa  26307  abelth  26424  efif1olem4  26527  eflog  26558  logef  26563  logeftb  26565  dvrelog  26619  dvlog  26633  cxpcn3  26730  efrlim  26951  eflgam  27026  wilthlem3  27051  basellem8  27069  lgsqrlem1  27327  noetasuplem4  27718  noetainflem4  27722  precsexlem1  28217  precsexlem2  28218  precsexlem3  28219  precsexlem4  28220  precsexlem5  28221  tgcgr4  28617  krippenlem  28776  colperpexlem1  28816  opphllem3  28835  lmiisolem  28882  axlowdimlem8  29036  axlowdimlem9  29037  axlowdimlem11  29039  axlowdimlem12  29040  axlowdimlem17  29045  ushgredgedg  29316  ushgredgedgloop  29318  subgruhgredgd  29371  vtxdlfgrval  29572  vtxd0nedgb  29575  vtxdushgrfvedg  29577  vtxdginducedm1lem3  29628  finsumvtxdg2size  29637  vtxdgoddnumeven  29640  isrgr  29646  fusgrregdegfi  29656  wlk1walk  29725  wlkres  29755  wlkp1lem5  29762  wlkp1lem6  29763  wlkp1lem7  29764  wlkp1lem8  29765  clwlkcompbp  29868  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  2wlkdlem3  30013  2wlkdlem8  30019  2wlkond  30023  umgr2adedgwlk  30031  1wlkdlem4  30228  1pthond  30232  wlk2v2elem2  30244  3wlkdlem3  30249  3wlkdlem8  30255  3cycld  30266  3cyclpd  30267  eucrctshift  30331  frgrncvvdeq  30397  frgrwopreglem2  30401  ex-fpar  30550  avril1  30551  vafval  30692  smfval  30694  0vfval  30695  nmcvfval  30696  vsfval  30722  hhssabloilem  31350  pjoc2i  31527  pjcji  31773  ho0val  31839  hoival  31844  adjbdlnb  32173  nmopcoadji  32190  opsqrlem2  32230  opsqrlem5  32233  hmopidmchi  32240  hmopidmpji  32241  pjinvari  32280  pjadj2coi  32293  pj3lem1  32295  pmtrprfv2  33169  cycpmco2lem7  33213  evl1fpws  33647  mplmulmvr  33723  evlextv  33726  esplyfval1  33757  esplyfvaln  33758  esplyind  33759  esplyindfv  33760  esplyfvn  33761  vietalem  33763  rtelextdg2lem  33910  constr0  33921  constrsuc  33922  constrlim  33923  2sqr3minply  33964  cos9thpiminplylem6  33971  madjusmdetlem1  34011  cnre2csqlem  34094  zzsnm  34143  rrhcn  34181  qqhre  34204  oms0  34481  omsmon  34482  omssubaddlem  34483  omssubadd  34484  eulerpart  34566  fib0  34583  fib1  34584  fibp1  34585  coinflippv  34668  gsumnunsn  34725  2cycld  35366  derangenlem  35399  kur14lem2  35435  kur14lem3  35436  kur14lem5  35438  kur14lem6  35439  txsconnlem  35468  cvmliftlem4  35516  cvmliftlem5  35517  satf0sucom  35601  satf0suc  35604  satf0op  35605  fmla  35609  satffunlem2lem2  35634  satfv0fvfmla0  35641  sate0  35643  funpartfv  36173  fullfunfv  36175  sumeq2si  36430  prodeq2si  36432  cbvprodvw2  36475  neibastop2lem  36588  dffinxpf  37747  ftc1cnnc  38059  heiborlem4  38181  heiborlem6  38183  cdlemk13  41344  cdlemk14  41346  cdlemk15  41347  cdlemk21N  41365  cdlemk20  41366  cdlemk56w  41465  lcfrlem1  42034  hdmapfval  42319  deg1gprod  42625  rabdiophlem2  43247  dnnumch1  43489  aomclem6  43504  mncn0  43584  aaitgo  43607  rngunsnply  43614  cytpval  43647  dssmapntrcls  44572  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  binomcxp  44801  fvmpt2df  45716  fsumsermpt  46024  fmul01  46025  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  lptioo2cn  46088  lptioo1cn  46089  limclner  46094  dvsinax  46356  fperdvper  46362  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  itgsin0pilem1  46393  stoweidlem3  46446  stoweidlem17  46460  stoweidlem47  46490  fourierdlem42  46592  fourierdlem62  46611  fourierdlem80  46629  fourierdlem90  46639  fourierdlem92  46641  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  fouriercnp  46669  sge0isum  46870  sge0seq  46889  ovnsubadd  47015  vonn0ioo  47130  vonn0icc  47131  smflimsup  47271  cjnpoly  47352  sinnpoly  47354  fcores  47530  fundcmpsurinjimaid  47886  isgrim  48373  gricushgr  48408  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem6  48591  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem10  48595  rhmsubcALTVlem2  48773  ply1mulgsum  48881  lineval  48885  lincvalpr  48909  lindslinindimp2lem4  48952  zlmodzxzldeplem3  48993  zlmodzxzldeplem4  48994  itcoval0mpt  49157  ackvalsuc1mpt  49169  ackval0  49171  ackval40  49184  ackval41a  49185  ackval42  49187  ackval50  49189  ehl2eudisval0  49216  2sphere0  49241  line2  49243  line2x  49245  line2y  49246  itscnhlinecirc02p  49276  oppcup  49697  natoppf  49719