Theorem fveq12d 6899

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 6894	. 2 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
3		fveq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	fveq2d 6896	. 2 ⊢ (𝜑 → (𝐺‘𝐴) = (𝐺‘𝐵))
5	2, 4	eqtrd 2773	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552

This theorem is referenced by:  nffvd  6904  fvmpopr2d  7569  wrecseq123OLD  8300  tfrlem3a  8377  resixpfo  8930  cantnfval  9663  cantnfres  9672  fseqenlem1  10019  fseqenlem2  10020  dfac12lem1  10138  dfac12lem2  10139  dfac12r  10141  hsmexlem2  10422  ttukeylem3  10506  ttukey2g  10511  seq1  13979  expval  14029  lsw  14514  ccatfval  14523  swrdval  14593  splfv2a  14706  revval  14710  relexpsucnnr  14972  relexp1g  14973  seqshft  15032  climshft2  15526  fprodser  15893  imasval  17457  funcid  17820  funcco  17821  funcoppc  17825  funcres  17846  nati  17906  funcestrcsetclem7  18098  funcestrcsetclem9  18100  funcsetcestrclem7  18113  funcsetcestrclem9  18115  evlf2  18171  evlf1  18173  evlfcl  18175  uncf2  18190  hofcl  18212  yonedalem21  18226  yonedalem3a  18227  yonedalem4a  18228  yonedalem4b  18229  yonedalem22  18231  yonedalem3  18233  yonedainv  18234  p0val  18380  p1val  18381  gsumvalx  18595  gsumpropd  18597  gsumval2a  18604  gsumsgrpccat  18721  prdsinvlem  18932  mulgfval  18952  mulgfvalALT  18953  mulgval  18954  mulgnndir  18983  mulgpropd  18996  cntrval  19183  efgsf  19597  efgsval  19599  issrngd  20469  rlmval  20813  chrval  21077  znval  21087  isphl  21181  isphld  21207  phlpropd  21208  cssval  21235  prdsinvgd2  21297  islindf  21367  evlseu  21646  evlval  21658  selvffval  21679  selvval  21681  evls1fval  21838  evl1varpw  21880  madetsumid  21963  madufval  22139  smadiadetr  22177  decpmatval0  22266  chpmatfval  22332  isperf  22655  dfac14  23122  xkohmeo  23319  flffval  23493  fcfval  23537  cnextfval  23566  tsmsval2  23634  tsmspropd  23636  tngngp  24171  tngngp3  24173  isnlm  24192  sranlm  24201  cnncvsabsnegdemo  24682  ovoliunlem1  25019  ovoliunlem2  25020  limcfval  25389  dvfval  25414  dvreslem  25426  dvaddbr  25455  dvmulbr  25456  isuc1p  25658  ismon1p  25660  q1pval  25671  dgreq0  25779  vieta1lem2  25824  vieta1  25825  basellem5  26589  lgsval  26804  lgsneg  26824  israg  27979  iswlkon  28945  wlkres  28958  wlkp1lem3  28963  wlkp1lem6  28966  isclwlk  29061  iscrct  29078  iscycl  29079  eupth2eucrct  29501  dipfval  29986  splfv3  32153  cycpmco2lem5  32320  cycpmco2lem6  32321  idlsrgval  32648  extdgval  32764  minplyval  32797  lmatfval  32825  lmat22e11  32829  rrhval  33007  xrhval  33029  prodindf  33052  brae  33270  braew  33271  sitmval  33379  sseqval  33418  fibp1  33431  elprob  33439  signsvtn0  33612  signstfvneq0  33614  signstfveq0  33619  breprexplema  33673  breprexp  33676  circlevma  33685  circlemethhgt  33686  cvmliftlem5  34311  cvmliftlem7  34313  cvmliftlem10  34316  cvmliftlem13  34318  satefv  34436  mclsval  34585  rdgprc0  34796  dfrdg2  34798  gg-dvmulbr  35206  bj-finsumval0  36214  rdgeqoa  36299  finxpeq2  36316  finxpreclem6  36325  finxpsuclem  36326  sdclem2  36658  ldualvsub  38073  ldualvsubval  38075  isopos  38098  polfvalN  38823  psubclsetN  38855  docaffvalN  40040  docafvalN  40041  djaffvalN  40052  djafvalN  40053  dihffval  40149  dihfval  40150  dochffval  40268  dochfval  40269  djhffval  40315  djhfval  40316  islpolN  40402  lcdfval  40507  lcdval  40508  lcdvsub  40536  lcdvsubval  40537  mapdffval  40545  mapdfval  40546  hdmap1fval  40715  hdmapfval  40746  hgmapfval  40805  hdmapglem7  40848  hlhilset  40853  evlselv  41207  0prjspnrel  41417  ismrc  41487  rmxfval  41690  rmyfval  41691  aomclem8  41851  hbt  41920  elmnc  41926  mncn0  41929  aaitgo  41952  mon1pid  41995  clsk1independent  42845  binomcxp  43164  limciccioolb  44385  limcicciooub  44401  ioccncflimc  44649  icocncflimc  44653  dvnprodlem2  44711  dvnprodlem3  44712  dirkercncflem3  44869  fourierdlem32  44903  etransclem32  45030  etransclem44  45042  etransclem46  45044  etransc  45047  ovnsubaddlem1  45334  ovnsubaddlem2  45335  ovnsubadd  45336  hoidmvlelem4  45362  hoidmvlelem5  45363  hspmbl  45393  vonioo  45446  vonicc  45449  afveq12d  45889  iccelpart  46149  nnsum3primesprm  46506  isomgreqve  46541  funcringcsetcALTV2lem7  46988  funcringcsetcALTV2lem9  46990  funcringcsetclem7ALTV  47011  funcringcsetclem9ALTV  47013