Theorem fveq12d 6882

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6530

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  nffvd  6887  fvmpopr2d  7567  wrecseq123OLD  8312  tfrlem3a  8389  resixpfo  8948  cantnfval  9680  cantnfres  9689  fseqenlem1  10036  fseqenlem2  10037  dfac12lem1  10156  dfac12lem2  10157  dfac12r  10159  hsmexlem2  10439  ttukeylem3  10523  ttukey2g  10528  seq1  14030  expval  14079  lsw  14580  ccatfval  14589  swrdval  14659  splfv2a  14772  revval  14776  relexpsucnnr  15042  relexp1g  15043  seqshft  15102  climshft2  15596  fprodser  15963  imasval  17523  funcid  17881  funcco  17882  funcoppc  17886  funcres  17907  nati  17969  funcestrcsetclem7  18156  funcestrcsetclem9  18158  funcsetcestrclem7  18171  funcsetcestrclem9  18173  evlf2  18228  evlf1  18230  evlfcl  18232  uncf2  18247  hofcl  18269  yonedalem21  18283  yonedalem3a  18284  yonedalem4a  18285  yonedalem4b  18286  yonedalem22  18288  yonedalem3  18290  yonedainv  18291  p0val  18435  p1val  18436  gsumvalx  18652  gsumpropd  18654  gsumval2a  18661  gsumsgrpccat  18816  prdsinvlem  19030  mulgfval  19050  mulgfvalALT  19051  mulgval  19052  mulgnndir  19084  mulgpropd  19097  cntrval  19300  efgsf  19708  efgsval  19710  issrngd  20813  rlmval  21147  chrval  21482  znval  21494  isphl  21586  isphld  21612  phlpropd  21613  cssval  21640  prdsinvgd2  21700  islindf  21770  evlseu  22039  evlval  22051  selvffval  22069  selvval  22071  evls1fval  22255  evl1varpw  22297  madetsumid  22397  madufval  22573  smadiadetr  22611  decpmatval0  22700  chpmatfval  22766  isperf  23087  dfac14  23554  xkohmeo  23751  flffval  23925  fcfval  23969  cnextfval  23998  tsmsval2  24066  tsmspropd  24068  tngngp  24591  tngngp3  24593  isnlm  24612  sranlm  24621  cnncvsabsnegdemo  25115  ovoliunlem1  25453  ovoliunlem2  25454  limcfval  25823  dvfval  25848  dvreslem  25860  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  isuc1p  26096  ismon1p  26098  mon1pid  26109  q1pval  26110  dgreq0  26221  vieta1lem2  26269  vieta1  26270  basellem5  27045  lgsval  27262  lgsneg  27282  seqseq123d  28209  israg  28622  iswlkon  29583  wlkres  29596  wlkp1lem3  29601  wlkp1lem6  29604  isclwlk  29701  iscrct  29718  iscycl  29719  eupth2eucrct  30144  dipfval  30629  prodindf  32786  splfv3  32880  cycpmco2lem5  33087  cycpmco2lem6  33088  idlsrgval  33464  m1pmeq  33542  extdgval  33641  fldextrspundgle  33665  minplyval  33685  constrcon  33754  2sqr3minply  33760  lmatfval  33791  lmat22e11  33795  rrhval  33973  xrhval  33995  brae  34218  braew  34219  sitmval  34327  sseqval  34366  fibp1  34379  elprob  34387  signsvtn0  34548  signstfvneq0  34550  signstfveq0  34555  breprexplema  34608  breprexp  34611  circlevma  34620  circlemethhgt  34621  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  satefv  35382  mclsval  35531  rdgprc0  35757  dfrdg2  35759  bj-finsumval0  37249  rdgeqoa  37334  finxpeq2  37351  finxpreclem6  37360  finxpsuclem  37361  sdclem2  37712  ldualvsub  39119  ldualvsubval  39121  isopos  39144  polfvalN  39869  psubclsetN  39901  docaffvalN  41086  docafvalN  41087  djaffvalN  41098  djafvalN  41099  dihffval  41195  dihfval  41196  dochffval  41314  dochfval  41315  djhffval  41361  djhfval  41362  islpolN  41448  lcdfval  41553  lcdval  41554  lcdvsub  41582  lcdvsubval  41583  mapdffval  41591  mapdfval  41592  hdmap1fval  41761  hdmapfval  41792  hgmapfval  41851  hdmapglem7  41894  hlhilset  41899  aks6d1c1p1  42066  evlselv  42557  0prjspnrel  42597  ismrc  42671  rmxfval  42874  rmyfval  42875  aomclem8  43032  hbt  43101  elmnc  43107  mncn0  43110  aaitgo  43133  clsk1independent  44017  binomcxp  44329  limciccioolb  45598  limcicciooub  45614  ioccncflimc  45862  icocncflimc  45866  dvnprodlem2  45924  dvnprodlem3  45925  dirkercncflem3  46082  fourierdlem32  46116  etransclem32  46243  etransclem44  46255  etransclem46  46257  etransc  46260  ovnsubaddlem1  46547  ovnsubaddlem2  46548  ovnsubadd  46549  hoidmvlelem4  46575  hoidmvlelem5  46576  hspmbl  46606  vonioo  46659  vonicc  46662  afveq12d  47110  iccelpart  47395  nnsum3primesprm  47752  funcringcsetcALTV2lem7  48219  funcringcsetcALTV2lem9  48221  funcringcsetclem7ALTV  48242  funcringcsetclem9ALTV  48244  swapfida  49145  cofuswapf2  49154  fuco21  49195  fuco23  49200  fucoid  49207