Theorem fveq1i 6907

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

Syntax hints:   = wceq 1540  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  fveq12i  6912  fvun2  7001  fvopab3ig  7012  fvsnun1  7202  fvpr1g  7210  fvpr2g  7211  fvtp1  7215  fvtp2  7216  fvtp3  7217  fvtp1g  7218  fvtp2g  7219  fvtp3g  7220  fpropnf1  7287  fveqf1o  7322  ov  7577  ovigg  7578  ovg  7598  fvresex  7984  curry1  8129  curry2  8132  fsplitfpar  8143  suppsnop  8203  frrlem12  8322  fprlem1  8325  wfrlem5OLD  8353  tfr2a  8435  rdgsucmptf  8468  rdgsucmptnf  8469  frsucmpt  8478  frsucmptn  8479  seqomlem1  8490  seqomlem3  8492  seqomlem4  8493  seqom0g  8496  seqomsuc  8497  unblem2  9329  inf3lemb  9665  inf3lemc  9666  ttrclselem1  9765  ttrclselem2  9766  trcl  9768  frrlem15  9797  r10  9808  r1sucg  9809  r1limg  9811  infxpenc2  10062  aleph0  10106  alephlim  10107  alephsuc  10108  alephfplem1  10144  alephfplem2  10145  ackbij2lem3  10280  cfsmolem  10310  infpssrlem1  10343  infpssrlem2  10344  fin23lem34  10386  fin23lem35  10387  isf32lem6  10398  isf32lem7  10399  isf32lem8  10400  isf34lem5  10418  hsmexlem7  10463  axdclem2  10560  canthp1lem2  10693  wunex2  10778  wuncval2  10787  addpiord  10924  mulpiord  10925  addpqnq  10978  mulpqnq  10981  fseq1p1m1  13638  om2uz0i  13988  om2uzrdg  13997  uzrdg0i  14000  uzrdgsuci  14001  hashkf  14371  hashgval  14372  hashinf  14374  ccat1st1st  14666  revs1  14803  cats1fv  14898  shftidt  15121  cbvsum  15731  cbvsumv  15732  fsumss  15761  isumclim3  15795  isumsup2  15882  cbvprod  15949  cbvprodv  15950  fprodss  15984  iprodclim3  16036  fprodefsum  16131  ruclem4  16270  ruclem6  16271  ruclem7  16272  sadc0  16491  sadcp1  16492  sadcaddlem  16494  sadaddlem  16503  smup0  16516  smupp1  16517  algr0  16609  algrp1  16611  ndxarg  17233  strfv2d  17238  funcoppc  17920  fthepi  17975  homadm  18085  homacd  18086  prdsidlem  18782  prdsinvlem  19067  cayleylem2  19431  symggen  19488  pmtr3ncomlem1  19491  gsumval3  19925  gsumzaddlem  19939  gsumzmhm  19955  pgpfaclem1  20101  ringidval  20180  rhmsubclem2  20686  lidlval  21220  rspval  21221  lidlnegcl  21232  lpival  21334  znf1o  21570  ply1ascl0  22256  ply1ascl1  22257  eqcoe1ply1eq  22303  evls1val  22324  evl1val  22333  mat1dimmul  22482  mdetralt  22614  mdetunilem7  22624  decpmatid  22776  pmatcollpwscmatlem1  22795  cpmidpmat  22879  chcoeffeq  22892  restcls  23189  restntr  23190  upxp  23631  cnmetdval  24791  remetdval  24810  qdensere2  24818  pcoptcl  25054  pcopt  25055  pcopt2  25056  pcorevlem  25059  isncvsngp  25183  cnncvsabsnegdemo  25199  ovolfsval  25505  ovollb2lem  25523  ovolunlem1a  25531  ovoliunlem1  25537  ovoliun2  25541  ovolscalem1  25548  ovolicc2lem4  25555  mblvol  25565  ioombl1lem4  25596  uniioovol  25614  uniioombllem3  25620  0pval  25706  limccnp  25926  limccnp2  25927  dvcnvrelem2  26057  itgsubstlem  26089  ply1remlem  26204  plyrem  26347  qaa  26365  abelth  26485  efif1olem4  26587  eflog  26618  logef  26623  logeftb  26625  dvrelog  26679  dvlog  26693  cxpcn3  26791  efrlim  27012  efrlimOLD  27013  eflgam  27088  wilthlem3  27113  basellem8  27131  lgsqrlem1  27390  noetasuplem4  27781  noetainflem4  27785  precsexlem1  28231  precsexlem2  28232  precsexlem3  28233  precsexlem4  28234  precsexlem5  28235  tgcgr4  28539  krippenlem  28698  colperpexlem1  28738  opphllem3  28757  lmiisolem  28804  axlowdimlem8  28964  axlowdimlem9  28965  axlowdimlem11  28967  axlowdimlem12  28968  axlowdimlem17  28973  ushgredgedg  29246  ushgredgedgloop  29248  subgruhgredgd  29301  vtxdlfgrval  29503  vtxd0nedgb  29506  vtxdushgrfvedg  29508  vtxdginducedm1lem3  29559  finsumvtxdg2size  29568  vtxdgoddnumeven  29571  isrgr  29577  fusgrregdegfi  29587  wlk1walk  29657  wlkres  29688  wlkp1lem5  29695  wlkp1lem6  29696  wlkp1lem7  29697  wlkp1lem8  29698  clwlkcompbp  29802  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  2wlkdlem3  29947  2wlkdlem8  29953  2wlkond  29957  umgr2adedgwlk  29965  1wlkdlem4  30159  1pthond  30163  wlk2v2elem2  30175  3wlkdlem3  30180  3wlkdlem8  30186  3cycld  30197  3cyclpd  30198  eucrctshift  30262  frgrncvvdeq  30328  frgrwopreglem2  30332  ex-fpar  30481  avril1  30482  vafval  30622  smfval  30624  0vfval  30625  nmcvfval  30626  vsfval  30652  hhssabloilem  31280  pjoc2i  31457  pjcji  31703  ho0val  31769  hoival  31774  adjbdlnb  32103  nmopcoadji  32120  opsqrlem2  32160  opsqrlem5  32163  hmopidmchi  32170  hmopidmpji  32171  pjinvari  32210  pjadj2coi  32223  pj3lem1  32225  funcnvmpt  32677  pmtrprfv2  33108  cycpmco2lem7  33152  evl1fpws  33590  rgmoddimOLD  33661  rtelextdg2lem  33767  constr0  33778  constrsuc  33779  constrlim  33780  2sqr3minply  33791  madjusmdetlem1  33826  cnre2csqlem  33909  zzsnm  33958  rrhcn  33998  qqhre  34021  oms0  34299  omsmon  34300  omssubaddlem  34301  omssubadd  34302  eulerpart  34384  fib0  34401  fib1  34402  fibp1  34403  coinflippv  34486  gsumnunsn  34556  2cycld  35143  derangenlem  35176  kur14lem2  35212  kur14lem3  35213  kur14lem5  35215  kur14lem6  35216  txsconnlem  35245  cvmliftlem4  35293  cvmliftlem5  35294  satf0sucom  35378  satf0suc  35381  satf0op  35382  fmla  35386  satffunlem2lem2  35411  satfv0fvfmla0  35418  sate0  35420  funpartfv  35946  fullfunfv  35948  sumeq2si  36203  prodeq2si  36205  cbvprodvw2  36248  neibastop2lem  36361  dffinxpf  37386  ftc1cnnc  37699  heiborlem4  37821  heiborlem6  37823  cdlemk13  40854  cdlemk14  40856  cdlemk15  40857  cdlemk21N  40875  cdlemk20  40876  cdlemk56w  40975  lcfrlem1  41544  hdmapfval  41829  deg1gprod  42141  evlsevl  42581  selvvvval  42595  rabdiophlem2  42813  dnnumch1  43056  aomclem6  43071  mncn0  43151  aaitgo  43174  rngunsnply  43181  cytpval  43214  dssmapntrcls  44141  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  binomcxp  44376  fvcod  45232  fvmpt2df  45279  fsumsermpt  45594  fmul01  45595  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  lptioo2cn  45660  lptioo1cn  45661  limclner  45666  dvsinax  45928  fperdvper  45934  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  itgsin0pilem1  45965  stoweidlem3  46018  stoweidlem17  46032  stoweidlem47  46062  fourierdlem42  46164  fourierdlem62  46183  fourierdlem80  46201  fourierdlem90  46211  fourierdlem92  46213  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fouriercnp  46241  sge0isum  46442  sge0seq  46461  ovnsubadd  46587  vonn0ioo  46702  vonn0icc  46703  smflimsup  46843  fcores  47079  fundcmpsurinjimaid  47398  isgrim  47868  gricushgr  47886  rhmsubcALTVlem2  48198  ply1mulgsum  48307  lineval  48311  lincvalpr  48335  lindslinindimp2lem4  48378  zlmodzxzldeplem3  48419  zlmodzxzldeplem4  48420  itcoval0mpt  48587  ackvalsuc1mpt  48599  ackval0  48601  ackval40  48614  ackval41a  48615  ackval42  48617  ackval50  48619  ehl2eudisval0  48646  2sphere0  48671  line2  48673  line2x  48675  line2y  48676  itscnhlinecirc02p  48706  oppcup  48948