Theorem fveq12d 6811

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466

This theorem is referenced by:  nffvd  6816  fvmpopr2d  7466  wrecseq123OLD  8162  tfrlem3a  8239  resixpfo  8755  cantnfval  9470  cantnfres  9479  fseqenlem1  9826  fseqenlem2  9827  dfac12lem1  9945  dfac12lem2  9946  dfac12r  9948  hsmexlem2  10229  ttukeylem3  10313  ttukey2g  10318  seq1  13780  expval  13830  lsw  14312  ccatfval  14321  swrdval  14401  splfv2a  14514  revval  14518  relexpsucnnr  14781  relexp1g  14782  seqshft  14841  climshft2  15336  fprodser  15704  imasval  17267  funcid  17630  funcco  17631  funcoppc  17635  funcres  17656  nati  17716  funcestrcsetclem7  17908  funcestrcsetclem9  17910  funcsetcestrclem7  17923  funcsetcestrclem9  17925  evlf2  17981  evlf1  17983  evlfcl  17985  uncf2  18000  hofcl  18022  yonedalem21  18036  yonedalem3a  18037  yonedalem4a  18038  yonedalem4b  18039  yonedalem22  18041  yonedalem3  18043  yonedainv  18044  p0val  18190  p1val  18191  gsumvalx  18405  gsumpropd  18407  gsumval2a  18414  gsumsgrpccat  18523  gsumccatOLD  18524  prdsinvlem  18729  mulgfval  18747  mulgfvalALT  18748  mulgval  18749  mulgnndir  18777  mulgpropd  18790  cntrval  18970  efgsf  19380  efgsval  19382  issrngd  20166  rlmval  20506  chrval  20774  znval  20784  isphl  20878  isphld  20904  phlpropd  20905  cssval  20932  prdsinvgd2  20994  islindf  21064  evlseu  21338  evlval  21350  selvffval  21371  selvval  21373  evls1fval  21530  evl1varpw  21572  madetsumid  21655  madufval  21831  smadiadetr  21869  decpmatval0  21958  chpmatfval  22024  isperf  22347  dfac14  22814  xkohmeo  23011  flffval  23185  fcfval  23229  cnextfval  23258  tsmsval2  23326  tsmspropd  23328  tngngp  23863  tngngp3  23865  isnlm  23884  sranlm  23893  cnncvsabsnegdemo  24374  ovoliunlem1  24711  ovoliunlem2  24712  limcfval  25081  dvfval  25106  dvreslem  25118  dvaddbr  25147  dvmulbr  25148  isuc1p  25350  ismon1p  25352  q1pval  25363  dgreq0  25471  vieta1lem2  25516  vieta1  25517  basellem5  26279  lgsval  26494  lgsneg  26514  israg  27103  iswlkon  28070  wlkres  28083  wlkp1lem3  28088  wlkp1lem6  28091  isclwlk  28186  iscrct  28203  iscycl  28204  eupth2eucrct  28626  dipfval  29109  splfv3  31275  cycpmco2lem5  31442  cycpmco2lem6  31443  idlsrgval  31693  extdgval  31774  lmatfval  31809  lmat22e11  31813  rrhval  31991  xrhval  32013  prodindf  32036  brae  32254  braew  32255  sitmval  32361  sseqval  32400  fibp1  32413  elprob  32421  signsvtn0  32594  signstfvneq0  32596  signstfveq0  32601  breprexplema  32655  breprexp  32658  circlevma  32667  circlemethhgt  32668  cvmliftlem5  33296  cvmliftlem7  33298  cvmliftlem10  33301  cvmliftlem13  33303  satefv  33421  mclsval  33570  rdgprc0  33814  dfrdg2  33816  bj-finsumval0  35500  rdgeqoa  35585  finxpeq2  35602  finxpreclem6  35611  finxpsuclem  35612  sdclem2  35944  ldualvsub  37211  ldualvsubval  37213  isopos  37236  polfvalN  37960  psubclsetN  37992  docaffvalN  39177  docafvalN  39178  djaffvalN  39189  djafvalN  39190  dihffval  39286  dihfval  39287  dochffval  39405  dochfval  39406  djhffval  39452  djhfval  39453  islpolN  39539  lcdfval  39644  lcdval  39645  lcdvsub  39673  lcdvsubval  39674  mapdffval  39682  mapdfval  39683  hdmap1fval  39852  hdmapfval  39883  hgmapfval  39942  hdmapglem7  39985  hlhilset  39990  0prjspnrel  40501  ismrc  40560  rmxfval  40763  rmyfval  40764  aomclem8  40924  hbt  40993  elmnc  40999  mncn0  41002  aaitgo  41025  mon1pid  41068  clsk1independent  41694  binomcxp  42013  limciccioolb  43211  limcicciooub  43227  ioccncflimc  43475  icocncflimc  43479  dvnprodlem2  43537  dvnprodlem3  43538  dirkercncflem3  43695  fourierdlem32  43729  etransclem32  43856  etransclem44  43868  etransclem46  43870  etransc  43873  ovnsubaddlem1  44158  ovnsubaddlem2  44159  ovnsubadd  44160  hoidmvlelem4  44186  hoidmvlelem5  44187  hspmbl  44217  vonioo  44270  vonicc  44273  afveq12d  44683  iccelpart  44943  nnsum3primesprm  45300  isomgreqve  45335  funcringcsetcALTV2lem7  45658  funcringcsetcALTV2lem9  45660  funcringcsetclem7ALTV  45681  funcringcsetclem9ALTV  45683