Theorem fveq1i 6843

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

Syntax hints:   = wceq 1542  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  fveq12i  6848  fvun2  6934  fvopab3ig  6945  funcnvmpt  6951  fvsnun1  7138  fvpr1g  7146  fvpr2g  7147  fvtp1  7151  fvtp2  7152  fvtp3  7153  fvtp1g  7154  fvtp2g  7155  fvtp3g  7156  fpropnf1  7223  fveqf1o  7258  ov  7512  ovigg  7513  ovg  7533  fvresex  7914  curry1  8056  curry2  8059  fsplitfpar  8070  suppsnop  8130  frrlem12  8249  fprlem1  8252  tfr2a  8336  rdgsucmptf  8369  rdgsucmptnf  8370  frsucmpt  8379  frsucmptn  8380  seqomlem1  8391  seqomlem3  8393  seqomlem4  8394  seqom0g  8397  seqomsuc  8398  unblem2  9205  inf3lemb  9546  inf3lemc  9547  ttrclselem1  9646  ttrclselem2  9647  trcl  9649  frrlem15  9681  r10  9692  r1sucg  9693  r1limg  9695  infxpenc2  9944  aleph0  9988  alephlim  9989  alephsuc  9990  alephfplem1  10026  alephfplem2  10027  ackbij2lem3  10162  cfsmolem  10192  infpssrlem1  10225  infpssrlem2  10226  fin23lem34  10268  fin23lem35  10269  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  isf34lem5  10300  hsmexlem7  10345  axdclem2  10442  canthp1lem2  10576  wunex2  10661  wuncval2  10670  addpiord  10807  mulpiord  10808  addpqnq  10861  mulpqnq  10864  fseq1p1m1  13526  om2uz0i  13882  om2uzrdg  13891  uzrdg0i  13894  uzrdgsuci  13895  hashkf  14267  hashgval  14268  hashinf  14270  ccat1st1st  14564  revs1  14700  cats1fv  14794  shftidt  15017  cbvsum  15630  cbvsumv  15631  fsumss  15660  isumclim3  15694  isumsup2  15781  cbvprod  15848  cbvprodv  15849  fprodss  15883  iprodclim3  15935  fprodefsum  16030  ruclem4  16171  ruclem6  16172  ruclem7  16173  sadc0  16393  sadcp1  16394  sadcaddlem  16396  sadaddlem  16405  smup0  16418  smupp1  16419  algr0  16511  algrp1  16513  ndxarg  17135  strfv2d  17140  funcoppc  17811  fthepi  17866  homadm  17976  homacd  17977  prdsidlem  18706  prdsinvlem  18991  cayleylem2  19354  symggen  19411  pmtr3ncomlem1  19414  gsumval3  19848  gsumzaddlem  19862  gsumzmhm  19878  pgpfaclem1  20024  ringidval  20130  rhmsubclem2  20631  lidlval  21177  rspval  21178  lidlnegcl  21189  lpival  21291  znf1o  21518  ply1ascl0  22207  ply1ascl1  22208  eqcoe1ply1eq  22255  evls1val  22276  evl1val  22285  mat1dimmul  22432  mdetralt  22564  mdetunilem7  22574  decpmatid  22726  pmatcollpwscmatlem1  22745  cpmidpmat  22829  chcoeffeq  22842  restcls  23137  restntr  23138  upxp  23579  cnmetdval  24726  remetdval  24745  qdensere2  24753  pcoptcl  24989  pcopt  24990  pcopt2  24991  pcorevlem  24994  isncvsngp  25117  cnncvsabsnegdemo  25133  ovolfsval  25439  ovollb2lem  25457  ovolunlem1a  25465  ovoliunlem1  25471  ovoliun2  25475  ovolscalem1  25482  ovolicc2lem4  25489  mblvol  25499  ioombl1lem4  25530  uniioovol  25548  uniioombllem3  25554  0pval  25640  limccnp  25860  limccnp2  25861  dvcnvrelem2  25991  itgsubstlem  26023  ply1remlem  26138  plyrem  26281  qaa  26299  abelth  26419  efif1olem4  26522  eflog  26553  logef  26558  logeftb  26560  dvrelog  26614  dvlog  26628  cxpcn3  26726  efrlim  26947  efrlimOLD  26948  eflgam  27023  wilthlem3  27048  basellem8  27066  lgsqrlem1  27325  noetasuplem4  27716  noetainflem4  27720  precsexlem1  28215  precsexlem2  28216  precsexlem3  28217  precsexlem4  28218  precsexlem5  28219  tgcgr4  28615  krippenlem  28774  colperpexlem1  28814  opphllem3  28833  lmiisolem  28880  axlowdimlem8  29034  axlowdimlem9  29035  axlowdimlem11  29037  axlowdimlem12  29038  axlowdimlem17  29043  ushgredgedg  29314  ushgredgedgloop  29316  subgruhgredgd  29369  vtxdlfgrval  29571  vtxd0nedgb  29574  vtxdushgrfvedg  29576  vtxdginducedm1lem3  29627  finsumvtxdg2size  29636  vtxdgoddnumeven  29639  isrgr  29645  fusgrregdegfi  29655  wlk1walk  29724  wlkres  29754  wlkp1lem5  29761  wlkp1lem6  29762  wlkp1lem7  29763  wlkp1lem8  29764  clwlkcompbp  29867  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  2wlkdlem3  30012  2wlkdlem8  30018  2wlkond  30022  umgr2adedgwlk  30030  1wlkdlem4  30227  1pthond  30231  wlk2v2elem2  30243  3wlkdlem3  30248  3wlkdlem8  30254  3cycld  30265  3cyclpd  30266  eucrctshift  30330  frgrncvvdeq  30396  frgrwopreglem2  30400  ex-fpar  30549  avril1  30550  vafval  30691  smfval  30693  0vfval  30694  nmcvfval  30695  vsfval  30721  hhssabloilem  31349  pjoc2i  31526  pjcji  31772  ho0val  31838  hoival  31843  adjbdlnb  32172  nmopcoadji  32189  opsqrlem2  32229  opsqrlem5  32232  hmopidmchi  32239  hmopidmpji  32240  pjinvari  32279  pjadj2coi  32292  pj3lem1  32294  pmtrprfv2  33182  cycpmco2lem7  33226  evl1fpws  33657  mplmulmvr  33716  evlextv  33719  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  esplyindfv  33753  esplyfvn  33754  vietalem  33756  rgmoddimOLD  33788  rtelextdg2lem  33904  constr0  33915  constrsuc  33916  constrlim  33917  2sqr3minply  33958  cos9thpiminplylem6  33965  madjusmdetlem1  34005  cnre2csqlem  34088  zzsnm  34137  rrhcn  34175  qqhre  34198  oms0  34475  omsmon  34476  omssubaddlem  34477  omssubadd  34478  eulerpart  34560  fib0  34577  fib1  34578  fibp1  34579  coinflippv  34662  gsumnunsn  34719  2cycld  35354  derangenlem  35387  kur14lem2  35423  kur14lem3  35424  kur14lem5  35426  kur14lem6  35427  txsconnlem  35456  cvmliftlem4  35504  cvmliftlem5  35505  satf0sucom  35589  satf0suc  35592  satf0op  35593  fmla  35597  satffunlem2lem2  35622  satfv0fvfmla0  35629  sate0  35631  funpartfv  36161  fullfunfv  36163  sumeq2si  36418  prodeq2si  36420  cbvprodvw2  36463  neibastop2lem  36576  dffinxpf  37640  ftc1cnnc  37943  heiborlem4  38065  heiborlem6  38067  cdlemk13  41228  cdlemk14  41230  cdlemk15  41231  cdlemk21N  41249  cdlemk20  41250  cdlemk56w  41349  lcfrlem1  41918  hdmapfval  42203  deg1gprod  42510  evlsevl  42932  selvvvval  42943  rabdiophlem2  43159  dnnumch1  43401  aomclem6  43416  mncn0  43496  aaitgo  43519  rngunsnply  43526  cytpval  43559  dssmapntrcls  44484  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  binomcxp  44713  fvcod  45585  fvmpt2df  45630  fsumsermpt  45939  fmul01  45940  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  lptioo2cn  46003  lptioo1cn  46004  limclner  46009  dvsinax  46271  fperdvper  46277  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  dvnprodlem3  46306  itgsin0pilem1  46308  stoweidlem3  46361  stoweidlem17  46375  stoweidlem47  46405  fourierdlem42  46507  fourierdlem62  46526  fourierdlem80  46544  fourierdlem90  46554  fourierdlem92  46556  fourierdlem93  46557  fourierdlem103  46567  fourierdlem104  46568  fouriercnp  46584  sge0isum  46785  sge0seq  46804  ovnsubadd  46930  vonn0ioo  47045  vonn0icc  47046  smflimsup  47186  cjnpoly  47249  sinnpoly  47251  fcores  47427  fundcmpsurinjimaid  47771  isgrim  48242  gricushgr  48277  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem6  48460  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem10  48464  rhmsubcALTVlem2  48642  ply1mulgsum  48750  lineval  48754  lincvalpr  48778  lindslinindimp2lem4  48821  zlmodzxzldeplem3  48862  zlmodzxzldeplem4  48863  itcoval0mpt  49026  ackvalsuc1mpt  49038  ackval0  49040  ackval40  49053  ackval41a  49054  ackval42  49056  ackval50  49058  ehl2eudisval0  49085  2sphere0  49110  line2  49112  line2x  49114  line2y  49115  itscnhlinecirc02p  49145  oppcup  49566  natoppf  49588