Theorem fveq12d 6724

Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)

Hypotheses

Ref	Expression
fveq12d.1	⊢ (𝜑 → 𝐹 = 𝐺)
fveq12d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveq12d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Proof of Theorem fveq12d

Step	Hyp	Ref	Expression
1		fveq12d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	fveq1d 6719	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
3		fveq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	fveq2d 6721	. 2 ⊢ (𝜑 → (𝐺‘𝐴) = (𝐺‘𝐵))
5	2, 4	eqtrd 2777	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Syntax hints:   → wi 4   = wceq 1543  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388

This theorem is referenced by:  nffvd  6729  fvmpopr2d  7370  wrecseq123  8048  tfrlem3a  8113  resixpfo  8617  cantnfval  9283  cantnfres  9292  fseqenlem1  9638  fseqenlem2  9639  dfac12lem1  9757  dfac12lem2  9758  dfac12r  9760  hsmexlem2  10041  ttukeylem3  10125  ttukey2g  10130  seq1  13587  expval  13637  lsw  14119  ccatfval  14128  swrdval  14208  splfv2a  14321  revval  14325  relexpsucnnr  14588  relexp1g  14589  seqshft  14648  climshft2  15143  fprodser  15511  imasval  17016  funcid  17376  funcco  17377  funcoppc  17381  funcres  17402  nati  17462  funcestrcsetclem7  17653  funcestrcsetclem9  17655  funcsetcestrclem7  17668  funcsetcestrclem9  17670  evlf2  17726  evlf1  17728  evlfcl  17730  uncf2  17745  hofcl  17767  yonedalem21  17781  yonedalem3a  17782  yonedalem4a  17783  yonedalem4b  17784  yonedalem22  17786  yonedalem3  17788  yonedainv  17789  p0val  17933  p1val  17934  gsumvalx  18148  gsumpropd  18150  gsumval2a  18157  gsumsgrpccat  18266  gsumccatOLD  18267  prdsinvlem  18472  mulgfval  18490  mulgfvalALT  18491  mulgval  18492  mulgnndir  18520  mulgpropd  18533  cntrval  18713  efgsf  19119  efgsval  19121  issrngd  19897  rlmval  20228  chrval  20490  znval  20500  isphl  20590  isphld  20616  phlpropd  20617  cssval  20644  prdsinvgd2  20704  islindf  20774  evlseu  21043  evlval  21055  selvffval  21076  selvval  21078  evls1fval  21235  evl1varpw  21277  madetsumid  21358  madufval  21534  smadiadetr  21572  decpmatval0  21661  chpmatfval  21727  isperf  22048  dfac14  22515  xkohmeo  22712  flffval  22886  fcfval  22930  cnextfval  22959  tsmsval2  23027  tsmspropd  23029  tngngp  23552  tngngp3  23554  isnlm  23573  sranlm  23582  cnncvsabsnegdemo  24062  ovoliunlem1  24399  ovoliunlem2  24400  limcfval  24769  dvfval  24794  dvreslem  24806  dvaddbr  24835  dvmulbr  24836  isuc1p  25038  ismon1p  25040  q1pval  25051  dgreq0  25159  vieta1lem2  25204  vieta1  25205  basellem5  25967  lgsval  26182  lgsneg  26202  israg  26788  iswlkon  27745  wlkres  27758  wlkp1lem3  27763  wlkp1lem6  27766  isclwlk  27860  iscrct  27877  iscycl  27878  eupth2eucrct  28300  dipfval  28783  splfv3  30950  cycpmco2lem5  31116  cycpmco2lem6  31117  idlsrgval  31362  extdgval  31443  lmatfval  31478  lmat22e11  31482  rrhval  31658  xrhval  31680  prodindf  31703  brae  31921  braew  31922  sitmval  32028  sseqval  32067  fibp1  32080  elprob  32088  signsvtn0  32261  signstfvneq0  32263  signstfveq0  32268  breprexplema  32322  breprexp  32325  circlevma  32334  circlemethhgt  32335  cvmliftlem5  32964  cvmliftlem7  32966  cvmliftlem10  32969  cvmliftlem13  32971  satefv  33089  mclsval  33238  rdgprc0  33488  dfrdg2  33490  bj-finsumval0  35191  rdgeqoa  35278  finxpeq2  35295  finxpreclem6  35304  finxpsuclem  35305  sdclem2  35637  ldualvsub  36906  ldualvsubval  36908  isopos  36931  polfvalN  37655  psubclsetN  37687  docaffvalN  38872  docafvalN  38873  djaffvalN  38884  djafvalN  38885  dihffval  38981  dihfval  38982  dochffval  39100  dochfval  39101  djhffval  39147  djhfval  39148  islpolN  39234  lcdfval  39339  lcdval  39340  lcdvsub  39368  lcdvsubval  39369  mapdffval  39377  mapdfval  39378  hdmap1fval  39547  hdmapfval  39578  hgmapfval  39637  hdmapglem7  39680  hlhilset  39685  0prjspnrel  40172  ismrc  40226  rmxfval  40429  rmyfval  40430  aomclem8  40589  hbt  40658  elmnc  40664  mncn0  40667  aaitgo  40690  mon1pid  40733  clsk1independent  41333  binomcxp  41648  limciccioolb  42837  limcicciooub  42853  ioccncflimc  43101  icocncflimc  43105  dvnprodlem2  43163  dvnprodlem3  43164  dirkercncflem3  43321  fourierdlem32  43355  etransclem32  43482  etransclem44  43494  etransclem46  43496  etransc  43499  ovnsubaddlem1  43783  ovnsubaddlem2  43784  ovnsubadd  43785  hoidmvlelem4  43811  hoidmvlelem5  43812  hspmbl  43842  vonioo  43895  vonicc  43898  afveq12d  44297  iccelpart  44558  nnsum3primesprm  44915  isomgreqve  44950  funcringcsetcALTV2lem7  45273  funcringcsetcALTV2lem9  45275  funcringcsetclem7ALTV  45296  funcringcsetclem9ALTV  45298