Theorem fveq1i 6921

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

Syntax hints:   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  fveq12i  6926  fvun2  7014  fvopab3ig  7025  fvsnun1  7216  fvpr1g  7224  fvpr2g  7225  fvpr2gOLD  7226  fvpr1OLD  7228  fvpr2OLD  7230  fvtp1  7232  fvtp2  7233  fvtp3  7234  fvtp1g  7235  fvtp2g  7236  fvtp3g  7237  fpropnf1  7304  fveqf1o  7338  ov  7594  ovigg  7595  ovg  7615  fvresex  8000  curry1  8145  curry2  8148  fsplitfpar  8159  suppsnop  8219  frrlem12  8338  fprlem1  8341  wfrlem5OLD  8369  tfr2a  8451  rdgsucmptf  8484  rdgsucmptnf  8485  frsucmpt  8494  frsucmptn  8495  seqomlem1  8506  seqomlem3  8508  seqomlem4  8509  seqom0g  8512  seqomsuc  8513  unblem2  9357  inf3lemb  9694  inf3lemc  9695  ttrclselem1  9794  ttrclselem2  9795  trcl  9797  frrlem15  9826  r10  9837  r1sucg  9838  r1limg  9840  infxpenc2  10091  aleph0  10135  alephlim  10136  alephsuc  10137  alephfplem1  10173  alephfplem2  10174  ackbij2lem3  10309  cfsmolem  10339  infpssrlem1  10372  infpssrlem2  10373  fin23lem34  10415  fin23lem35  10416  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  isf34lem5  10447  hsmexlem7  10492  axdclem2  10589  canthp1lem2  10722  wunex2  10807  wuncval2  10816  addpiord  10953  mulpiord  10954  addpqnq  11007  mulpqnq  11010  fseq1p1m1  13658  om2uz0i  13998  om2uzrdg  14007  uzrdg0i  14010  uzrdgsuci  14011  hashkf  14381  hashgval  14382  hashinf  14384  ccat1st1st  14676  revs1  14813  cats1fv  14908  shftidt  15131  cbvsum  15743  cbvsumv  15744  fsumss  15773  isumclim3  15807  isumsup2  15894  cbvprod  15961  cbvprodv  15962  fprodss  15996  iprodclim3  16048  fprodefsum  16143  ruclem4  16282  ruclem6  16283  ruclem7  16284  sadc0  16500  sadcp1  16501  sadcaddlem  16503  sadaddlem  16512  smup0  16525  smupp1  16526  algr0  16619  algrp1  16621  ndxarg  17243  strfv2d  17249  funcoppc  17939  fthepi  17995  homadm  18107  homacd  18108  prdsidlem  18804  prdsinvlem  19089  cayleylem2  19455  symggen  19512  pmtr3ncomlem1  19515  gsumval3  19949  gsumzaddlem  19963  gsumzmhm  19979  pgpfaclem1  20125  ringidval  20210  rhmsubclem2  20708  lidlval  21243  rspval  21244  lidlnegcl  21255  lpival  21357  znf1o  21593  ply1ascl0  22277  ply1ascl1  22278  eqcoe1ply1eq  22324  evls1val  22345  evl1val  22354  mat1dimmul  22503  mdetralt  22635  mdetunilem7  22645  decpmatid  22797  pmatcollpwscmatlem1  22816  cpmidpmat  22900  chcoeffeq  22913  restcls  23210  restntr  23211  upxp  23652  cnmetdval  24812  remetdval  24830  qdensere2  24838  pcoptcl  25073  pcopt  25074  pcopt2  25075  pcorevlem  25078  isncvsngp  25202  cnncvsabsnegdemo  25218  ovolfsval  25524  ovollb2lem  25542  ovolunlem1a  25550  ovoliunlem1  25556  ovoliun2  25560  ovolscalem1  25567  ovolicc2lem4  25574  mblvol  25584  ioombl1lem4  25615  uniioovol  25633  uniioombllem3  25639  0pval  25725  limccnp  25946  limccnp2  25947  dvcnvrelem2  26077  itgsubstlem  26109  ply1remlem  26224  plyrem  26365  qaa  26383  abelth  26503  efif1olem4  26605  eflog  26636  logef  26641  logeftb  26643  dvrelog  26697  dvlog  26711  cxpcn3  26809  efrlim  27030  efrlimOLD  27031  eflgam  27106  wilthlem3  27131  basellem8  27149  lgsqrlem1  27408  noetasuplem4  27799  noetainflem4  27803  precsexlem1  28249  precsexlem2  28250  precsexlem3  28251  precsexlem4  28252  precsexlem5  28253  tgcgr4  28557  krippenlem  28716  colperpexlem1  28756  opphllem3  28775  lmiisolem  28822  axlowdimlem8  28982  axlowdimlem9  28983  axlowdimlem11  28985  axlowdimlem12  28986  axlowdimlem17  28991  ushgredgedg  29264  ushgredgedgloop  29266  subgruhgredgd  29319  vtxdlfgrval  29521  vtxd0nedgb  29524  vtxdushgrfvedg  29526  vtxdginducedm1lem3  29577  finsumvtxdg2size  29586  vtxdgoddnumeven  29589  isrgr  29595  fusgrregdegfi  29605  wlk1walk  29675  wlkres  29706  wlkp1lem5  29713  wlkp1lem6  29714  wlkp1lem7  29715  wlkp1lem8  29716  clwlkcompbp  29818  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  2wlkdlem3  29960  2wlkdlem8  29966  2wlkond  29970  umgr2adedgwlk  29978  1wlkdlem4  30172  1pthond  30176  wlk2v2elem2  30188  3wlkdlem3  30193  3wlkdlem8  30199  3cycld  30210  3cyclpd  30211  eucrctshift  30275  frgrncvvdeq  30341  frgrwopreglem2  30345  ex-fpar  30494  avril1  30495  vafval  30635  smfval  30637  0vfval  30638  nmcvfval  30639  vsfval  30665  hhssabloilem  31293  pjoc2i  31470  pjcji  31716  ho0val  31782  hoival  31787  adjbdlnb  32116  nmopcoadji  32133  opsqrlem2  32173  opsqrlem5  32176  hmopidmchi  32183  hmopidmpji  32184  pjinvari  32223  pjadj2coi  32236  pj3lem1  32238  funcnvmpt  32685  pmtrprfv2  33081  cycpmco2lem7  33125  evl1fpws  33555  rgmoddimOLD  33623  rtelextdg2lem  33717  constr0  33727  constrsuc  33728  constrlim  33729  2sqr3minply  33738  madjusmdetlem1  33773  cnre2csqlem  33856  zzsnm  33905  rrhcn  33943  qqhre  33966  oms0  34262  omsmon  34263  omssubaddlem  34264  omssubadd  34265  eulerpart  34347  fib0  34364  fib1  34365  fibp1  34366  coinflippv  34448  gsumnunsn  34518  2cycld  35106  derangenlem  35139  kur14lem2  35175  kur14lem3  35176  kur14lem5  35178  kur14lem6  35179  txsconnlem  35208  cvmliftlem4  35256  cvmliftlem5  35257  satf0sucom  35341  satf0suc  35344  satf0op  35345  fmla  35349  satffunlem2lem2  35374  satfv0fvfmla0  35381  sate0  35383  funpartfv  35909  fullfunfv  35911  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36213  neibastop2lem  36326  dffinxpf  37351  ftc1cnnc  37652  heiborlem4  37774  heiborlem6  37776  cdlemk13  40809  cdlemk14  40811  cdlemk15  40812  cdlemk21N  40830  cdlemk20  40831  cdlemk56w  40930  lcfrlem1  41499  hdmapfval  41784  deg1gprod  42097  evlsevl  42526  selvvvval  42540  rabdiophlem2  42758  dnnumch1  43001  aomclem6  43016  mncn0  43096  aaitgo  43119  rngunsnply  43130  cytpval  43163  dssmapntrcls  44090  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  binomcxp  44326  fvcod  45134  fvmpt2df  45182  fsumsermpt  45500  fmul01  45501  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  lptioo2cn  45566  lptioo1cn  45567  limclner  45572  dvsinax  45834  fperdvper  45840  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  itgsin0pilem1  45871  stoweidlem3  45924  stoweidlem17  45938  stoweidlem47  45968  fourierdlem42  46070  fourierdlem62  46089  fourierdlem80  46107  fourierdlem90  46117  fourierdlem92  46119  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fouriercnp  46147  sge0isum  46348  sge0seq  46367  ovnsubadd  46493  vonn0ioo  46608  vonn0icc  46609  smflimsup  46749  fcores  46982  fundcmpsurinjimaid  47285  isgrim  47752  gricushgr  47770  rhmsubcALTVlem2  48005  ply1mulgsum  48119  lineval  48123  lincvalpr  48147  lindslinindimp2lem4  48190  zlmodzxzldeplem3  48231  zlmodzxzldeplem4  48232  itcoval0mpt  48400  ackvalsuc1mpt  48412  ackval0  48414  ackval40  48427  ackval41a  48428  ackval42  48430  ackval50  48432  ehl2eudisval0  48459  2sphere0  48484  line2  48486  line2x  48488  line2y  48489  itscnhlinecirc02p  48519