Theorem fveq1i 6827

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

Syntax hints:   = wceq 1540  ‘cfv 6486

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494

This theorem is referenced by:  fveq12i  6832  fvun2  6919  fvopab3ig  6930  fvsnun1  7122  fvpr1g  7130  fvpr2g  7131  fvtp1  7135  fvtp2  7136  fvtp3  7137  fvtp1g  7138  fvtp2g  7139  fvtp3g  7140  fpropnf1  7208  fveqf1o  7243  ov  7497  ovigg  7498  ovg  7518  fvresex  7902  curry1  8044  curry2  8047  fsplitfpar  8058  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  9198  inf3lemb  9540  inf3lemc  9541  ttrclselem1  9640  ttrclselem2  9641  trcl  9643  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  10566  wunex2  10651  wuncval2  10660  addpiord  10797  mulpiord  10798  addpqnq  10851  mulpqnq  10854  fseq1p1m1  13520  om2uz0i  13873  om2uzrdg  13882  uzrdg0i  13885  uzrdgsuci  13886  hashkf  14258  hashgval  14259  hashinf  14261  ccat1st1st  14554  revs1  14690  cats1fv  14785  shftidt  15008  cbvsum  15621  cbvsumv  15622  fsumss  15651  isumclim3  15685  isumsup2  15772  cbvprod  15839  cbvprodv  15840  fprodss  15874  iprodclim3  15926  fprodefsum  16021  ruclem4  16162  ruclem6  16163  ruclem7  16164  sadc0  16384  sadcp1  16385  sadcaddlem  16387  sadaddlem  16396  smup0  16409  smupp1  16410  algr0  16502  algrp1  16504  ndxarg  17126  strfv2d  17131  funcoppc  17801  fthepi  17856  homadm  17966  homacd  17967  prdsidlem  18662  prdsinvlem  18947  cayleylem2  19311  symggen  19368  pmtr3ncomlem1  19371  gsumval3  19805  gsumzaddlem  19819  gsumzmhm  19835  pgpfaclem1  19981  ringidval  20087  rhmsubclem2  20590  lidlval  21136  rspval  21137  lidlnegcl  21148  lpival  21250  znf1o  21477  ply1ascl0  22156  ply1ascl1  22157  eqcoe1ply1eq  22203  evls1val  22224  evl1val  22233  mat1dimmul  22380  mdetralt  22512  mdetunilem7  22522  decpmatid  22674  pmatcollpwscmatlem1  22693  cpmidpmat  22777  chcoeffeq  22790  restcls  23085  restntr  23086  upxp  23527  cnmetdval  24675  remetdval  24694  qdensere2  24702  pcoptcl  24938  pcopt  24939  pcopt2  24940  pcorevlem  24943  isncvsngp  25066  cnncvsabsnegdemo  25082  ovolfsval  25388  ovollb2lem  25406  ovolunlem1a  25414  ovoliunlem1  25420  ovoliun2  25424  ovolscalem1  25431  ovolicc2lem4  25438  mblvol  25448  ioombl1lem4  25479  uniioovol  25497  uniioombllem3  25503  0pval  25589  limccnp  25809  limccnp2  25810  dvcnvrelem2  25940  itgsubstlem  25972  ply1remlem  26087  plyrem  26230  qaa  26248  abelth  26368  efif1olem4  26471  eflog  26502  logef  26507  logeftb  26509  dvrelog  26563  dvlog  26577  cxpcn3  26675  efrlim  26896  efrlimOLD  26897  eflgam  26972  wilthlem3  26997  basellem8  27015  lgsqrlem1  27274  noetasuplem4  27665  noetainflem4  27669  precsexlem1  28133  precsexlem2  28134  precsexlem3  28135  precsexlem4  28136  precsexlem5  28137  tgcgr4  28495  krippenlem  28654  colperpexlem1  28694  opphllem3  28713  lmiisolem  28760  axlowdimlem8  28913  axlowdimlem9  28914  axlowdimlem11  28916  axlowdimlem12  28917  axlowdimlem17  28922  ushgredgedg  29193  ushgredgedgloop  29195  subgruhgredgd  29248  vtxdlfgrval  29450  vtxd0nedgb  29453  vtxdushgrfvedg  29455  vtxdginducedm1lem3  29506  finsumvtxdg2size  29515  vtxdgoddnumeven  29518  isrgr  29524  fusgrregdegfi  29534  wlk1walk  29603  wlkres  29633  wlkp1lem5  29640  wlkp1lem6  29641  wlkp1lem7  29642  wlkp1lem8  29643  clwlkcompbp  29746  crctcshwlkn0lem4  29777  crctcshwlkn0lem5  29778  crctcshwlkn0lem6  29779  2wlkdlem3  29891  2wlkdlem8  29897  2wlkond  29901  umgr2adedgwlk  29909  1wlkdlem4  30103  1pthond  30107  wlk2v2elem2  30119  3wlkdlem3  30124  3wlkdlem8  30130  3cycld  30141  3cyclpd  30142  eucrctshift  30206  frgrncvvdeq  30272  frgrwopreglem2  30276  ex-fpar  30425  avril1  30426  vafval  30566  smfval  30568  0vfval  30569  nmcvfval  30570  vsfval  30596  hhssabloilem  31224  pjoc2i  31401  pjcji  31647  ho0val  31713  hoival  31718  adjbdlnb  32047  nmopcoadji  32064  opsqrlem2  32104  opsqrlem5  32107  hmopidmchi  32114  hmopidmpji  32115  pjinvari  32154  pjadj2coi  32167  pj3lem1  32169  funcnvmpt  32629  pmtrprfv2  33049  cycpmco2lem7  33093  evl1fpws  33518  rgmoddimOLD  33596  rtelextdg2lem  33712  constr0  33723  constrsuc  33724  constrlim  33725  2sqr3minply  33766  cos9thpiminplylem6  33773  madjusmdetlem1  33813  cnre2csqlem  33896  zzsnm  33945  rrhcn  33983  qqhre  34006  oms0  34284  omsmon  34285  omssubaddlem  34286  omssubadd  34287  eulerpart  34369  fib0  34386  fib1  34387  fibp1  34388  coinflippv  34471  gsumnunsn  34528  2cycld  35130  derangenlem  35163  kur14lem2  35199  kur14lem3  35200  kur14lem5  35202  kur14lem6  35203  txsconnlem  35232  cvmliftlem4  35280  cvmliftlem5  35281  satf0sucom  35365  satf0suc  35368  satf0op  35369  fmla  35373  satffunlem2lem2  35398  satfv0fvfmla0  35405  sate0  35407  funpartfv  35938  fullfunfv  35940  sumeq2si  36195  prodeq2si  36197  cbvprodvw2  36240  neibastop2lem  36353  dffinxpf  37378  ftc1cnnc  37691  heiborlem4  37813  heiborlem6  37815  cdlemk13  40851  cdlemk14  40853  cdlemk15  40854  cdlemk21N  40872  cdlemk20  40873  cdlemk56w  40972  lcfrlem1  41541  hdmapfval  41826  deg1gprod  42133  evlsevl  42564  selvvvval  42578  rabdiophlem2  42795  dnnumch1  43037  aomclem6  43052  mncn0  43132  aaitgo  43155  rngunsnply  43162  cytpval  43195  dssmapntrcls  44121  binomcxplemdvsum  44348  binomcxplemnotnn0  44349  binomcxp  44350  fvcod  45225  fvmpt2df  45270  fsumsermpt  45580  fmul01  45581  fmuldfeq  45584  fmul01lt1lem1  45585  fmul01lt1lem2  45586  lptioo2cn  45646  lptioo1cn  45647  limclner  45652  dvsinax  45914  fperdvper  45920  dvnmul  45944  dvnprodlem1  45947  dvnprodlem2  45948  dvnprodlem3  45949  itgsin0pilem1  45951  stoweidlem3  46004  stoweidlem17  46018  stoweidlem47  46048  fourierdlem42  46150  fourierdlem62  46169  fourierdlem80  46187  fourierdlem90  46197  fourierdlem92  46199  fourierdlem93  46200  fourierdlem103  46210  fourierdlem104  46211  fouriercnp  46227  sge0isum  46428  sge0seq  46447  ovnsubadd  46573  vonn0ioo  46688  vonn0icc  46689  smflimsup  46829  cjnpoly  46893  sinnpoly  46895  fcores  47071  fundcmpsurinjimaid  47415  isgrim  47886  gricushgr  47921  gpgprismgr4cycllem3  48101  gpgprismgr4cycllem6  48104  gpgprismgr4cycllem7  48105  gpgprismgr4cycllem10  48108  rhmsubcALTVlem2  48286  ply1mulgsum  48395  lineval  48399  lincvalpr  48423  lindslinindimp2lem4  48466  zlmodzxzldeplem3  48507  zlmodzxzldeplem4  48508  itcoval0mpt  48671  ackvalsuc1mpt  48683  ackval0  48685  ackval40  48698  ackval41a  48699  ackval42  48701  ackval50  48703  ehl2eudisval0  48730  2sphere0  48755  line2  48757  line2x  48759  line2y  48760  itscnhlinecirc02p  48790  oppcup  49212  natoppf  49234