Theorem fveq1i 6784

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

Syntax hints:   = wceq 1539  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  fveq12i  6789  fvun2  6869  fvopab3ig  6880  fvsnun1  7063  fvpr1g  7071  fvpr2g  7072  fvpr2gOLD  7073  fvpr1OLD  7075  fvpr2OLD  7077  fvtp1  7079  fvtp2  7080  fvtp3  7081  fvtp1g  7082  fvtp2g  7083  fvtp3g  7084  fpropnf1  7149  fveqf1o  7184  ov  7426  ovigg  7427  ovg  7446  fvresex  7811  curry1  7953  curry2  7956  fsplitfpar  7968  suppsnop  8003  frrlem12  8122  fprlem1  8125  wfrlem5OLD  8153  tfr2a  8235  rdgsucmptf  8268  rdgsucmptnf  8269  frsucmpt  8278  frsucmptn  8279  seqomlem1  8290  seqomlem3  8292  seqomlem4  8293  seqom0g  8296  seqomsuc  8297  unblem2  9076  inf3lemb  9392  inf3lemc  9393  ttrclselem1  9492  ttrclselem2  9493  trcl  9495  frrlem15  9524  r10  9535  r1sucg  9536  r1limg  9538  infxpenc2  9787  aleph0  9831  alephlim  9832  alephsuc  9833  alephfplem1  9869  alephfplem2  9870  ackbij2lem3  10006  cfsmolem  10035  infpssrlem1  10068  infpssrlem2  10069  fin23lem34  10111  fin23lem35  10112  isf32lem6  10123  isf32lem7  10124  isf32lem8  10125  isf34lem5  10143  hsmexlem7  10188  axdclem2  10285  canthp1lem2  10418  wunex2  10503  wuncval2  10512  addpiord  10649  mulpiord  10650  addpqnq  10703  mulpqnq  10706  fseq1p1m1  13339  om2uz0i  13676  om2uzrdg  13685  uzrdg0i  13688  uzrdgsuci  13689  hashkf  14055  hashgval  14056  hashinf  14058  ccat1st1st  14344  revs1  14487  cats1fv  14581  shftidt  14802  cbvsum  15416  fsumss  15446  isumclim3  15480  isumsup2  15567  cbvprod  15634  fprodss  15667  iprodclim3  15719  fprodefsum  15813  ruclem4  15952  ruclem6  15953  ruclem7  15954  sadc0  16170  sadcp1  16171  sadcaddlem  16173  sadaddlem  16182  smup0  16195  smupp1  16196  algr0  16286  algrp1  16288  ndxarg  16906  strfv2d  16912  funcoppc  17599  fthepi  17653  homadm  17764  homacd  17765  prdsidlem  18426  prdsinvlem  18693  cayleylem2  19030  symggen  19087  pmtr3ncomlem1  19090  gsumval3  19517  gsumzaddlem  19531  gsumzmhm  19547  pgpfaclem1  19693  ringidval  19748  lidlval  20471  rspval  20472  lidlnegcl  20494  lpival  20525  znf1o  20768  eqcoe1ply1eq  21477  evls1val  21495  evl1val  21504  mat1dimmul  21634  mdetralt  21766  mdetunilem7  21776  decpmatid  21928  pmatcollpwscmatlem1  21947  cpmidpmat  22031  chcoeffeq  22044  restcls  22341  restntr  22342  upxp  22783  cnmetdval  23943  remetdval  23961  qdensere2  23969  pcoptcl  24193  pcopt  24194  pcopt2  24195  pcorevlem  24198  isncvsngp  24322  cnncvsabsnegdemo  24338  ovolfsval  24643  ovollb2lem  24661  ovolunlem1a  24669  ovoliunlem1  24675  ovoliun2  24679  ovolscalem1  24686  ovolicc2lem4  24693  mblvol  24703  ioombl1lem4  24734  uniioovol  24752  uniioombllem3  24758  0pval  24844  limccnp  25064  limccnp2  25065  dvcnvrelem2  25191  itgsubstlem  25221  ply1remlem  25336  plyrem  25474  qaa  25492  abelth  25609  efif1olem4  25710  eflog  25741  logef  25746  logeftb  25748  dvrelog  25801  dvlog  25815  cxpcn3  25910  efrlim  26128  eflgam  26203  wilthlem3  26228  basellem8  26246  lgsqrlem1  26503  tgcgr4  26901  krippenlem  27060  colperpexlem1  27100  opphllem3  27119  lmiisolem  27166  axlowdimlem8  27326  axlowdimlem9  27327  axlowdimlem11  27329  axlowdimlem12  27330  axlowdimlem17  27335  ushgredgedg  27605  ushgredgedgloop  27607  subgruhgredgd  27660  vtxdlfgrval  27861  vtxd0nedgb  27864  vtxdushgrfvedg  27866  vtxdginducedm1lem3  27917  finsumvtxdg2size  27926  vtxdgoddnumeven  27929  isrgr  27935  fusgrregdegfi  27945  wlk1walk  28015  wlkres  28047  wlkp1lem5  28054  wlkp1lem6  28055  wlkp1lem7  28056  wlkp1lem8  28057  clwlkcompbp  28159  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  2wlkdlem3  28301  2wlkdlem8  28307  2wlkond  28311  umgr2adedgwlk  28319  1wlkdlem4  28513  1pthond  28517  wlk2v2elem2  28529  3wlkdlem3  28534  3wlkdlem8  28540  3cycld  28551  3cyclpd  28552  eucrctshift  28616  frgrncvvdeq  28682  frgrwopreglem2  28686  ex-fpar  28835  avril1  28836  vafval  28974  smfval  28976  0vfval  28977  nmcvfval  28978  vsfval  29004  hhssabloilem  29632  pjoc2i  29809  pjcji  30055  ho0val  30121  hoival  30126  adjbdlnb  30455  nmopcoadji  30472  opsqrlem2  30512  opsqrlem5  30515  hmopidmchi  30522  hmopidmpji  30523  pjinvari  30562  pjadj2coi  30575  pj3lem1  30577  funcnvmpt  31013  pmtrprfv2  31366  cycpmco2lem7  31408  rgmoddim  31702  madjusmdetlem1  31786  cnre2csqlem  31869  zzsnm  31918  rrhcn  31956  qqhre  31979  oms0  32273  omsmon  32274  omssubaddlem  32275  omssubadd  32276  eulerpart  32358  fib0  32375  fib1  32376  fibp1  32377  coinflippv  32459  gsumnunsn  32529  2cycld  33109  derangenlem  33142  kur14lem2  33178  kur14lem3  33179  kur14lem5  33181  kur14lem6  33182  txsconnlem  33211  cvmliftlem4  33259  cvmliftlem5  33260  satf0sucom  33344  satf0suc  33347  satf0op  33348  fmla  33352  satffunlem2lem2  33377  satfv0fvfmla0  33384  sate0  33386  noetasuplem4  33948  noetainflem4  33952  funpartfv  34256  fullfunfv  34258  neibastop2lem  34558  dffinxpf  35565  ftc1cnnc  35858  heiborlem4  35981  heiborlem6  35983  cdlemk13  38873  cdlemk14  38875  cdlemk15  38876  cdlemk21N  38894  cdlemk20  38895  cdlemk56w  38994  lcfrlem1  39563  hdmapfval  39848  mplascl0  40277  rabdiophlem2  40631  dnnumch1  40876  aomclem6  40891  mncn0  40971  aaitgo  40994  rngunsnply  41005  cytpval  41041  dssmapntrcls  41745  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  binomcxp  41982  fvcod  42773  fsumsermpt  43127  fmul01  43128  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  lptioo2cn  43193  lptioo1cn  43194  limclner  43199  dvsinax  43461  fperdvper  43467  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  itgsin0pilem1  43498  stoweidlem3  43551  stoweidlem17  43565  stoweidlem47  43595  fourierdlem42  43697  fourierdlem62  43716  fourierdlem80  43734  fourierdlem90  43744  fourierdlem92  43746  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fouriercnp  43774  sge0isum  43972  sge0seq  43991  ovnsubadd  44117  vonn0ioo  44232  vonn0icc  44233  smflimsup  44372  fcores  44572  fundcmpsurinjimaid  44874  isomushgr  45289  rhmsubclem2  45656  rhmsubcALTVlem2  45674  ply1mulgsum  45742  lineval  45746  lincvalpr  45770  lindslinindimp2lem4  45813  zlmodzxzldeplem3  45854  zlmodzxzldeplem4  45855  itcoval0mpt  46023  ackvalsuc1mpt  46035  ackval0  46037  ackval40  46050  ackval41a  46051  ackval42  46053  ackval50  46055  ehl2eudisval0  46082  2sphere0  46107  line2  46109  line2x  46111  line2y  46112  itscnhlinecirc02p  46142