Theorem fveq12d 6884

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539

This theorem is used by:  nffvd  6889  fvmpopr2d  7574  tfrlem3a  8368  resixpfo  8948  cantnfval  9653  cantnfres  9662  fseqenlem1  10084  fseqenlem2  10085  dfac12lem1  10203  dfac12lem2  10204  dfac12r  10206  hsmexlem2  10486  ttukeylem3  10570  ttukey2g  10575  seq1  14137  expval  14186  lsw  14689  ccatfval  14698  swrdval  14771  splfv2a  14885  revval  14889  relexpsucnnr  15158  relexp1g  15159  seqshft  15218  climshft2  15729  fprodser  16096  imasval  17663  funcid  18025  funcco  18026  funcoppc  18030  funcres  18051  nati  18113  funcestrcsetclem7  18300  funcestrcsetclem9  18302  funcsetcestrclem7  18315  funcsetcestrclem9  18317  evlf2  18372  evlf1  18374  evlfcl  18376  uncf2  18391  hofcl  18413  yonedalem21  18427  yonedalem3a  18428  yonedalem4a  18429  yonedalem4b  18430  yonedalem22  18432  yonedalem3  18434  yonedainv  18435  p0val  18579  p1val  18580  gsumvalx  18845  gsumpropd  18847  gsumval2a  18854  gsumsgrpccat  19016  prdsinvlem  19239  mulgfval  19259  mulgfvalALT  19260  mulgval  19261  mulgnndir  19293  mulgpropd  19306  cntrval  19513  efgsf  19923  efgsval  19925  issrngd  21092  rlmval  21446  chrval  21809  znval  21821  isphl  21914  isphld  21940  phlpropd  21941  cssval  21968  prdsinvgd2  22028  islindf  22098  evlseu  22372  evlval  22389  selvffval  22407  selvval  22409  evls1fval  22617  evl1varpw  22659  madetsumid  22756  madufval  22932  smadiadetr  22970  decpmatval0  23062  chpmatfval  23128  isperf  23449  dfac14  23917  xkohmeo  24114  flffval  24288  fcfval  24332  cnextfval  24361  tsmsval2  24429  tsmspropd  24431  tngngp  24953  tngngp3  24955  isnlm  24974  sranlm  24983  cnncvsabsnegdemo  25466  ovoliunlem1  25803  ovoliunlem2  25804  limcfval  26172  dvfval  26197  dvreslem  26209  dvaddbr  26238  dvmulbr  26239  isuc1p  26439  ismon1p  26441  mon1pid  26452  q1pval  26453  dgreq0  26564  vieta1lem2  26616  vieta1  26617  basellem5  27394  lgsval  27610  lgsneg  27630  seqseq123d  28654  israg  29154  angmgmaddeu1  29361  iswlkon  30218  wlkres  30231  wlkp1lem3  30236  wlkp1lem6  30239  isclwlk  30342  iscrct  30359  iscycl  30360  eupth2eucrct  30800  dipfval  31286  prodindf  33411  splfv3  33501  cycpmco2lem5  33673  cycpmco2lem6  33674  idlsrgval  34017  m1pmeq  34099  mplvrpmfgalem  34158  mplvrpmga  34159  mplvrpmmhm  34160  mplvrpmrhm  34161  issply  34175  esplyval  34176  esplyind  34189  vieta  34194  extdgval  34267  fldextrspundgle  34292  minplyval  34319  constrcon  34388  2sqr3minply  34394  lmatfval  34428  lmat22e11  34432  rrhval  34610  xrhval  34632  brae  34856  braew  34857  sitmval  34964  sseqval  35003  fibp1  35016  elprob  35024  signsvtn0  35182  signstfvneq0  35184  signstfveq0  35189  breprexplema  35242  breprexp  35245  circlevma  35254  circlemethhgt  35255  cvmliftlem5  36023  cvmliftlem7  36025  cvmliftlem10  36028  cvmliftlem13  36030  satefv  36148  mclsval  36297  rdgprc0  36525  dfrdg2  36527  bj-finsumval0  38174  rdgeqoa  38261  finxpeq2  38278  finxpreclem6  38287  finxpsuclem  38288  sdclem2  38644  ldualvsub  40180  ldualvsubval  40182  isopos  40205  polfvalN  40929  psubclsetN  40961  docaffvalN  42146  docafvalN  42147  djaffvalN  42158  djafvalN  42159  dihffval  42255  dihfval  42256  dochffval  42374  dochfval  42375  djhffval  42421  djhfval  42422  islpolN  42508  lcdfval  42613  lcdval  42614  lcdvsub  42642  lcdvsubval  42643  mapdffval  42651  mapdfval  42652  hdmap1fval  42821  hdmapfval  42852  hgmapfval  42911  hdmapglem7  42954  hlhilset  42959  aks6d1c1p1  43125  evlselv  43579  0prjspnrel  43617  ismrc  43665  rmxfval  43864  rmyfval  43865  aomclem8  44021  hbt  44090  elmnc  44096  mncn0  44099  aaitgo  44122  clsk1independent  45005  binomcxp  45300  limciccioolb  46577  limcicciooub  46591  ioccncflimc  46839  icocncflimc  46843  dvnprodlem2  46901  dvnprodlem3  46902  dirkercncflem3  47059  fourierdlem32  47093  etransclem32  47220  etransclem44  47232  etransclem46  47234  etransc  47237  ovnsubaddlem1  47524  ovnsubaddlem2  47525  ovnsubadd  47526  hoidmvlelem4  47552  hoidmvlelem5  47553  hspmbl  47583  vonioo  47636  vonicc  47639  afveq12d  48147  iccelpart  48459  nnsum3primesprm  48832  funcringcsetcALTV2lem7  49337  funcringcsetcALTV2lem9  49339  funcringcsetclem7ALTV  49360  funcringcsetclem9ALTV  49362  cofu1a  50146  cofu2a  50147  cofid1  50166  cofid2  50167  uptr2  50273  swapfida  50332  cofuswapf2  50347  fuco21  50388  fuco23  50393  fucoid  50400  opf2  50458  oppfdiag1  50466  oppfdiag  50468  termolmd  50722