Theorem fveq12d 6890

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

Syntax hints:   → wi 4   = wceq 1570  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546

This theorem is referenced by:  nffvd  6895  fvmpopr2d  7574  tfrlem3a  8364  resixpfo  8935  cantnfval  9638  cantnfres  9647  fseqenlem1  10009  fseqenlem2  10010  dfac12lem1  10128  dfac12lem2  10129  dfac12r  10131  hsmexlem2  10412  ttukeylem3  10496  ttukey2g  10501  seq1  14052  expval  14101  lsw  14603  ccatfval  14612  swrdval  14683  splfv2a  14795  revval  14799  relexpsucnnr  15064  relexp1g  15065  seqshft  15124  climshft2  15635  fprodser  16005  imasval  17566  funcid  17928  funcco  17929  funcoppc  17933  funcres  17954  nati  18016  funcestrcsetclem7  18203  funcestrcsetclem9  18205  funcsetcestrclem7  18218  funcsetcestrclem9  18220  evlf2  18275  evlf1  18277  evlfcl  18279  uncf2  18294  hofcl  18316  yonedalem21  18330  yonedalem3a  18331  yonedalem4a  18332  yonedalem4b  18333  yonedalem22  18335  yonedalem3  18337  yonedainv  18338  p0val  18482  p1val  18483  gsumvalx  18735  gsumpropd  18737  gsumval2a  18744  gsumsgrpccat  18900  prdsinvlem  19116  mulgfval  19136  mulgfvalALT  19137  mulgval  19138  mulgnndir  19170  mulgpropd  19183  cntrval  19390  efgsf  19800  efgsval  19802  issrngd  20939  rlmval  21293  chrval  21654  znval  21666  isphl  21759  isphld  21785  phlpropd  21786  cssval  21813  prdsinvgd2  21873  islindf  21943  evlseu  22215  evlval  22232  selvffval  22250  selvval  22252  evls1fval  22460  evl1varpw  22502  madetsumid  22599  madufval  22775  smadiadetr  22813  decpmatval0  22902  chpmatfval  22968  isperf  23289  dfac14  23756  xkohmeo  23953  flffval  24127  fcfval  24171  cnextfval  24200  tsmsval2  24268  tsmspropd  24270  tngngp  24792  tngngp3  24794  isnlm  24813  sranlm  24822  cnncvsabsnegdemo  25305  ovoliunlem1  25642  ovoliunlem2  25643  limcfval  26012  dvfval  26037  dvreslem  26049  dvaddbr  26078  dvmulbr  26079  isuc1p  26279  ismon1p  26281  mon1pid  26292  q1pval  26293  dgreq0  26403  vieta1lem2  26453  vieta1  26454  basellem5  27230  lgsval  27446  lgsneg  27466  seqseq123d  28460  israg  28958  iswlkon  29986  wlkres  29999  wlkp1lem3  30004  wlkp1lem6  30007  isclwlk  30103  iscrct  30120  iscycl  30121  eupth2eucrct  30549  dipfval  31035  prodindf  33163  splfv3  33259  cycpmco2lem5  33431  cycpmco2lem6  33432  idlsrgval  33774  m1pmeq  33856  mplvrpmfgalem  33915  mplvrpmga  33916  mplvrpmmhm  33917  mplvrpmrhm  33918  issply  33932  esplyval  33933  esplyind  33946  vieta  33951  extdgval  34024  fldextrspundgle  34049  minplyval  34076  constrcon  34145  2sqr3minply  34151  lmatfval  34185  lmat22e11  34189  rrhval  34367  xrhval  34389  brae  34612  braew  34613  sitmval  34720  sseqval  34759  fibp1  34772  elprob  34780  signsvtn0  34938  signstfvneq0  34940  signstfveq0  34945  breprexplema  34998  breprexp  35001  circlevma  35010  circlemethhgt  35011  cvmliftlem5  35762  cvmliftlem7  35764  cvmliftlem10  35767  cvmliftlem13  35769  satefv  35887  mclsval  36036  rdgprc0  36264  dfrdg2  36266  bj-finsumval0  37910  rdgeqoa  37997  finxpeq2  38014  finxpreclem6  38023  finxpsuclem  38024  sdclem2  38374  ldualvsub  39910  ldualvsubval  39912  isopos  39935  polfvalN  40659  psubclsetN  40691  docaffvalN  41876  docafvalN  41877  djaffvalN  41888  djafvalN  41889  dihffval  41985  dihfval  41986  dochffval  42104  dochfval  42105  djhffval  42151  djhfval  42152  islpolN  42238  lcdfval  42343  lcdval  42344  lcdvsub  42372  lcdvsubval  42373  mapdffval  42381  mapdfval  42382  hdmap1fval  42551  hdmapfval  42582  hgmapfval  42641  hdmapglem7  42684  hlhilset  42689  aks6d1c1p1  42855  evlselv  43304  0prjspnrel  43342  ismrc  43415  rmxfval  43614  rmyfval  43615  aomclem8  43771  hbt  43840  elmnc  43846  mncn0  43849  aaitgo  43872  clsk1independent  44755  binomcxp  45050  limciccioolb  46320  limcicciooub  46334  ioccncflimc  46582  icocncflimc  46586  dvnprodlem2  46644  dvnprodlem3  46645  dirkercncflem3  46802  fourierdlem32  46836  etransclem32  46963  etransclem44  46975  etransclem46  46977  etransc  46980  ovnsubaddlem1  47267  ovnsubaddlem2  47268  ovnsubadd  47269  hoidmvlelem4  47295  hoidmvlelem5  47296  hspmbl  47326  vonioo  47379  vonicc  47382  afveq12d  47853  iccelpart  48165  nnsum3primesprm  48538  funcringcsetcALTV2lem7  49044  funcringcsetcALTV2lem9  49046  funcringcsetclem7ALTV  49067  funcringcsetclem9ALTV  49069  cofu1a  49855  cofu2a  49856  cofid1  49875  cofid2  49876  uptr2  49982  swapfida  50041  cofuswapf2  50056  fuco21  50097  fuco23  50102  fucoid  50109  opf2  50167  oppfdiag1  50175  oppfdiag  50177  termolmd  50431