Theorem fveq1i 6832

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

Syntax hints:   = wceq 1548  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497

This theorem is referenced by:  fveq12i  6837  fvun2  6923  fvcod  6930  fvopab3ig  6935  funcnvmpt  6941  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  8122  frrlem12  8241  fprlem1  8244  tfr2a  8328  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  seqomlem1  8383  seqomlem3  8385  seqomlem4  8386  seqom0g  8389  seqomsuc  8390  unblem2  9197  inf3lemb  9541  inf3lemc  9542  ttrclselem1  9641  ttrclselem2  9642  trcl  9644  frrlem15  9676  r10  9687  r1sucg  9688  r1limg  9690  infxpenc2  9939  aleph0  9983  alephlim  9984  alephsuc  9985  alephfplem1  10021  alephfplem2  10022  ackbij2lem3  10157  cfsmolem  10187  infpssrlem1  10220  infpssrlem2  10221  fin23lem34  10263  fin23lem35  10264  isf32lem6  10275  isf32lem7  10276  isf32lem8  10277  isf34lem5  10295  hsmexlem7  10340  axdclem2  10437  canthp1lem2  10571  wunex2  10656  wuncval2  10665  addpiord  10802  mulpiord  10803  addpqnq  10856  mulpqnq  10859  fseq1p1m1  13547  om2uz0i  13904  om2uzrdg  13913  uzrdg0i  13916  uzrdgsuci  13917  hashkf  14289  hashgval  14290  hashinf  14292  ccat1st1st  14586  revs1  14722  cats1fv  14816  shftidt  15039  cbvsum  15652  cbvsumv  15653  fsumss  15682  isumclim3  15716  indsumhash  15787  isumsup2  15806  cbvprod  15873  cbvprodv  15874  fprodss  15908  iprodclim3  15960  fprodefsum  16055  ruclem4  16196  ruclem6  16197  ruclem7  16198  sadc0  16418  sadcp1  16419  sadcaddlem  16421  sadaddlem  16430  smup0  16443  smupp1  16444  algr0  16536  algrp1  16538  ndxarg  17161  strfv2d  17166  funcoppc  17837  fthepi  17892  homadm  18002  homacd  18003  prdsidlem  18732  prdsinvlem  19020  cayleylem2  19383  symggen  19440  pmtr3ncomlem1  19443  gsumval3  19877  gsumzaddlem  19891  gsumzmhm  19907  pgpfaclem1  20053  ringidval  20159  rhmsubclem2  20662  lidlval  21207  rspval  21208  lidlnegcl  21219  lpival  21321  znf1o  21530  evlsevl  22112  selvvvval  22122  ply1ascl0  22243  ply1ascl1  22244  eqcoe1ply1eq  22289  evls1val  22310  evl1val  22319  mat1dimmul  22463  mdetralt  22595  mdetunilem7  22605  decpmatid  22757  pmatcollpwscmatlem1  22776  cpmidpmat  22860  chcoeffeq  22873  restcls  23168  restntr  23169  upxp  23610  cnmetdval  24757  remetdval  24776  qdensere2  24784  pcoptcl  25010  pcopt  25011  pcopt2  25012  pcorevlem  25015  isncvsngp  25138  cnncvsabsnegdemo  25154  ovolfsval  25459  ovollb2lem  25477  ovolunlem1a  25485  ovoliunlem1  25491  ovoliun2  25495  ovolscalem1  25502  ovolicc2lem4  25509  mblvol  25519  ioombl1lem4  25550  uniioovol  25568  uniioombllem3  25574  0pval  25660  limccnp  25880  limccnp2  25881  dvcnvrelem2  26007  itgsubstlem  26037  ply1remlem  26152  plyrem  26293  qaa  26311  abelth  26428  efif1olem4  26531  eflog  26562  logef  26567  logeftb  26569  dvrelog  26623  dvlog  26637  cxpcn3  26734  efrlim  26955  eflgam  27030  wilthlem3  27055  basellem8  27073  lgsqrlem1  27331  noetasuplem4  27722  noetainflem4  27726  precsexlem1  28221  precsexlem2  28222  precsexlem3  28223  precsexlem4  28224  precsexlem5  28225  tgcgr4  28621  krippenlem  28780  colperpexlem1  28820  opphllem3  28839  lmiisolem  28886  axlowdimlem8  29040  axlowdimlem9  29041  axlowdimlem11  29043  axlowdimlem12  29044  axlowdimlem17  29049  ushgredgedg  29320  ushgredgedgloop  29322  subgruhgredgd  29375  vtxdlfgrval  29576  vtxd0nedgb  29579  vtxdushgrfvedg  29581  vtxdginducedm1lem3  29632  finsumvtxdg2size  29641  vtxdgoddnumeven  29644  isrgr  29650  fusgrregdegfi  29660  wlk1walk  29729  wlkres  29759  wlkp1lem5  29766  wlkp1lem6  29767  wlkp1lem7  29768  wlkp1lem8  29769  clwlkcompbp  29872  crctcshwlkn0lem4  29903  crctcshwlkn0lem5  29904  crctcshwlkn0lem6  29905  2wlkdlem3  30017  2wlkdlem8  30023  2wlkond  30027  umgr2adedgwlk  30035  1wlkdlem4  30232  1pthond  30236  wlk2v2elem2  30248  3wlkdlem3  30253  3wlkdlem8  30259  3cycld  30270  3cyclpd  30271  eucrctshift  30335  frgrncvvdeq  30401  frgrwopreglem2  30405  ex-fpar  30554  avril1  30555  vafval  30696  smfval  30698  0vfval  30699  nmcvfval  30700  vsfval  30726  hhssabloilem  31354  pjoc2i  31531  pjcji  31777  ho0val  31843  hoival  31848  adjbdlnb  32177  nmopcoadji  32194  opsqrlem2  32234  opsqrlem5  32237  hmopidmchi  32244  hmopidmpji  32245  pjinvari  32284  pjadj2coi  32297  pj3lem1  32299  pmtrprfv2  33173  cycpmco2lem7  33217  evl1fpws  33659  mplmulmvr  33735  evlextv  33738  esplyfval1  33769  esplyfvaln  33770  esplyind  33771  esplyindfv  33772  esplyfvn  33773  vietalem  33775  rtelextdg2lem  33922  constr0  33933  constrsuc  33934  constrlim  33935  2sqr3minply  33976  cos9thpiminplylem6  33983  madjusmdetlem1  34023  cnre2csqlem  34106  zzsnm  34155  rrhcn  34193  qqhre  34216  oms0  34493  omsmon  34494  omssubaddlem  34495  omssubadd  34496  eulerpart  34578  fib0  34595  fib1  34596  fibp1  34597  coinflippv  34680  gsumnunsn  34737  2cycld  35381  derangenlem  35414  kur14lem2  35450  kur14lem3  35451  kur14lem5  35453  kur14lem6  35454  txsconnlem  35483  cvmliftlem4  35531  cvmliftlem5  35532  satf0sucom  35616  satf0suc  35619  satf0op  35620  fmla  35624  satffunlem2lem2  35649  satfv0fvfmla0  35656  sate0  35658  funpartfv  36188  fullfunfv  36190  sumeq2si  36445  prodeq2si  36447  cbvprodvw2  36490  neibastop2lem  36603  dffinxpf  37762  ftc1cnnc  38074  heiborlem4  38196  heiborlem6  38198  cdlemk13  41359  cdlemk14  41361  cdlemk15  41362  cdlemk21N  41380  cdlemk20  41381  cdlemk56w  41480  lcfrlem1  42049  hdmapfval  42334  deg1gprod  42640  rabdiophlem2  43262  dnnumch1  43504  aomclem6  43519  mncn0  43599  aaitgo  43622  rngunsnply  43629  cytpval  43662  dssmapntrcls  44587  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  binomcxp  44816  fvmpt2df  45730  fsumsermpt  46038  fmul01  46039  fmuldfeq  46042  fmul01lt1lem1  46043  fmul01lt1lem2  46044  lptioo2cn  46102  lptioo1cn  46103  limclner  46108  dvsinax  46370  fperdvper  46376  dvnmul  46400  dvnprodlem1  46403  dvnprodlem2  46404  dvnprodlem3  46405  itgsin0pilem1  46407  stoweidlem3  46460  stoweidlem17  46474  stoweidlem47  46504  fourierdlem42  46606  fourierdlem62  46625  fourierdlem80  46643  fourierdlem90  46653  fourierdlem92  46655  fourierdlem93  46656  fourierdlem103  46666  fourierdlem104  46667  fouriercnp  46683  sge0isum  46884  sge0seq  46903  ovnsubadd  47029  vonn0ioo  47144  vonn0icc  47145  smflimsup  47285  cjnpoly  47366  sinnpoly  47368  fcores  47544  fundcmpsurinjimaid  47900  isgrim  48387  gricushgr  48422  gpgprismgr4cycllem3  48602  gpgprismgr4cycllem6  48605  gpgprismgr4cycllem7  48606  gpgprismgr4cycllem10  48609  rhmsubcALTVlem2  48787  ply1mulgsum  48895  lineval  48899  lincvalpr  48923  lindslinindimp2lem4  48966  zlmodzxzldeplem3  49007  zlmodzxzldeplem4  49008  itcoval0mpt  49171  ackvalsuc1mpt  49183  ackval0  49185  ackval40  49198  ackval41a  49199  ackval42  49201  ackval50  49203  ehl2eudisval0  49230  2sphere0  49255  line2  49257  line2x  49259  line2y  49260  itscnhlinecirc02p  49290  oppcup  49711  natoppf  49733