Theorem fveq12d 6500

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

Syntax hints:   → wi 4   = wceq 1507  ‘cfv 6182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-iota 6146  df-fv 6190

This theorem is referenced by:  nffvd  6505  fvsngOLD  6762  wrecseq123  7744  tfrlem3a  7810  resixpfo  8289  cantnfval  8917  cantnfres  8926  fseqenlem1  9236  fseqenlem2  9237  dfac12lem1  9355  dfac12lem2  9356  dfac12r  9358  hsmexlem2  9639  ttukeylem3  9723  ttukey2g  9728  seq1  13190  expval  13239  lsw  13717  ccatfval  13726  swrdval  13796  splfv2a  13963  splfv2aOLD  13964  revval  13969  relexpsucnnr  14235  relexp1g  14236  seqshft  14295  climshft2  14790  fprodser  15153  imasval  16630  funcid  16988  funcco  16989  funcoppc  16993  funcres  17014  nati  17073  funcestrcsetclem7  17244  funcestrcsetclem9  17246  funcsetcestrclem7  17259  funcsetcestrclem9  17261  evlf2  17316  evlf1  17318  evlfcl  17320  uncf2  17335  hofcl  17357  yonedalem21  17371  yonedalem3a  17372  yonedalem4a  17373  yonedalem4b  17374  yonedalem22  17376  yonedalem3  17378  yonedainv  17379  p0val  17499  p1val  17500  gsumvalx  17728  gsumpropd  17730  gsumval2a  17737  gsumccat  17836  prdsinvlem  17985  mulgfval  18003  mulgfvalALT  18004  mulgval  18005  mulgnndir  18030  mulgpropd  18043  cntrval  18210  efgsf  18603  efgsval  18605  issrngd  19344  rlmval  19675  evlseu  19999  evlval  20007  evls1fval  20175  evl1varpw  20216  chrval  20364  znval  20374  isphl  20464  isphld  20490  phlpropd  20491  cssval  20518  prdsinvgd2  20578  islindf  20648  madetsumid  20764  madufval  20940  smadiadetr  20978  decpmatval0  21066  chpmatfval  21132  isperf  21453  dfac14  21920  xkohmeo  22117  flffval  22291  fcfval  22335  cnextfval  22364  tsmsval2  22431  tsmspropd  22433  tngngp  22956  tngngp3  22958  isnlm  22977  sranlm  22986  cnncvsabsnegdemo  23462  ovoliunlem1  23796  ovoliunlem2  23797  limcfval  24163  dvfval  24188  dvreslem  24200  dvaddbr  24228  dvmulbr  24229  isuc1p  24427  ismon1p  24429  q1pval  24440  dgreq0  24548  vieta1lem2  24593  vieta1  24594  basellem5  25354  lgsval  25569  lgsneg  25589  israg  26175  iswlkon  27131  wlkres  27146  wlkresOLD  27148  wlkp1lem3  27153  wlkp1lem6  27156  isclwlk  27252  iscrct  27269  iscycl  27270  eupth2eucrct  27737  dipfval  28246  extdgval  30629  lmatfval  30678  lmat22e11  30682  rrhval  30838  xrhval  30860  prodindf  30883  brae  31102  braew  31103  sitmval  31209  sseqval  31249  fibp1  31262  elprob  31270  signsvtn0  31447  signsvtn0OLD  31448  signstfvneq0  31450  signstfveq0  31455  signstfveq0OLD  31456  breprexplema  31510  breprexp  31513  circlevma  31522  circlemethhgt  31523  cvmliftlem5  32081  cvmliftlem7  32083  cvmliftlem10  32086  cvmliftlem13  32088  mclsval  32270  rdgprc0  32499  dfrdg2  32501  bj-finsumval0  33965  rdgeqoa  34028  finxpeq2  34044  finxpreclem6  34053  finxpsuclem  34054  sdclem2  34407  ldualvsub  35684  ldualvsubval  35686  isopos  35709  polfvalN  36433  psubclsetN  36465  docaffvalN  37650  docafvalN  37651  djaffvalN  37662  djafvalN  37663  dihffval  37759  dihfval  37760  dochffval  37878  dochfval  37879  djhffval  37925  djhfval  37926  islpolN  38012  lcdfval  38117  lcdval  38118  lcdvsub  38146  lcdvsubval  38147  mapdffval  38155  mapdfval  38156  hdmap1fval  38325  hdmapfval  38356  hgmapfval  38415  hdmapglem7  38458  hlhilset  38463  0prjspnrel  38621  ismrc  38638  rmxfval  38842  rmyfval  38843  aomclem8  39002  hbt  39071  elmnc  39077  mncn0  39080  aaitgo  39103  mon1pid  39146  clsk1independent  39704  binomcxp  40049  limciccioolb  41279  limcicciooub  41295  ioccncflimc  41544  icocncflimc  41548  dvnprodlem2  41608  dvnprodlem3  41609  dirkercncflem3  41767  fourierdlem32  41801  etransclem32  41928  etransclem44  41940  etransclem46  41942  etransc  41945  ovnsubaddlem1  42229  ovnsubaddlem2  42230  ovnsubadd  42231  hoidmvlelem4  42257  hoidmvlelem5  42258  hspmbl  42288  vonioo  42341  vonicc  42344  afveq12d  42684  iccelpart  42911  nnsum3primesprm  43263  isomgreqve  43298  funcringcsetcALTV2lem7  43617  funcringcsetcALTV2lem9  43619  funcringcsetclem7ALTV  43640  funcringcsetclem9ALTV  43642