Theorem fveq12d 6837

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6444  df-fv 6496

This theorem is referenced by:  nffvd  6842  fvmpopr2d  7516  tfrlem3a  8304  resixpfo  8868  cantnfval  9567  cantnfres  9576  fseqenlem1  9924  fseqenlem2  9925  dfac12lem1  10044  dfac12lem2  10045  dfac12r  10047  hsmexlem2  10327  ttukeylem3  10411  ttukey2g  10416  seq1  13925  expval  13974  lsw  14475  ccatfval  14484  swrdval  14555  splfv2a  14667  revval  14671  relexpsucnnr  14936  relexp1g  14937  seqshft  14996  climshft2  15493  fprodser  15860  imasval  17419  funcid  17781  funcco  17782  funcoppc  17786  funcres  17807  nati  17869  funcestrcsetclem7  18056  funcestrcsetclem9  18058  funcsetcestrclem7  18071  funcsetcestrclem9  18073  evlf2  18128  evlf1  18130  evlfcl  18132  uncf2  18147  hofcl  18169  yonedalem21  18183  yonedalem3a  18184  yonedalem4a  18185  yonedalem4b  18186  yonedalem22  18188  yonedalem3  18190  yonedainv  18191  p0val  18335  p1val  18336  gsumvalx  18588  gsumpropd  18590  gsumval2a  18597  gsumsgrpccat  18752  prdsinvlem  18966  mulgfval  18986  mulgfvalALT  18987  mulgval  18988  mulgnndir  19020  mulgpropd  19033  cntrval  19235  efgsf  19645  efgsval  19647  issrngd  20774  rlmval  21129  chrval  21464  znval  21476  isphl  21569  isphld  21595  phlpropd  21596  cssval  21623  prdsinvgd2  21683  islindf  21753  evlseu  22021  evlval  22033  selvffval  22051  selvval  22053  evls1fval  22237  evl1varpw  22279  madetsumid  22379  madufval  22555  smadiadetr  22593  decpmatval0  22682  chpmatfval  22748  isperf  23069  dfac14  23536  xkohmeo  23733  flffval  23907  fcfval  23951  cnextfval  23980  tsmsval2  24048  tsmspropd  24050  tngngp  24572  tngngp3  24574  isnlm  24593  sranlm  24602  cnncvsabsnegdemo  25095  ovoliunlem1  25433  ovoliunlem2  25434  limcfval  25803  dvfval  25828  dvreslem  25840  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  isuc1p  26076  ismon1p  26078  mon1pid  26089  q1pval  26090  dgreq0  26201  vieta1lem2  26249  vieta1  26250  basellem5  27025  lgsval  27242  lgsneg  27262  seqseq123d  28219  israg  28678  iswlkon  29638  wlkres  29651  wlkp1lem3  29656  wlkp1lem6  29659  isclwlk  29755  iscrct  29772  iscycl  29773  eupth2eucrct  30201  dipfval  30686  prodindf  32853  splfv3  32948  cycpmco2lem5  33108  cycpmco2lem6  33109  idlsrgval  33477  m1pmeq  33556  mplvrpmfgalem  33594  mplvrpmga  33595  mplvrpmmhm  33596  mplvrpmrhm  33597  issply  33604  esplyval  33605  esplyind  33615  extdgval  33689  fldextrspundgle  33714  minplyval  33741  constrcon  33810  2sqr3minply  33816  lmatfval  33850  lmat22e11  33854  rrhval  34032  xrhval  34054  brae  34277  braew  34278  sitmval  34385  sseqval  34424  fibp1  34437  elprob  34445  signsvtn0  34606  signstfvneq0  34608  signstfveq0  34613  breprexplema  34666  breprexp  34669  circlevma  34678  circlemethhgt  34679  cvmliftlem5  35356  cvmliftlem7  35358  cvmliftlem10  35361  cvmliftlem13  35363  satefv  35481  mclsval  35630  rdgprc0  35858  dfrdg2  35860  bj-finsumval0  37352  rdgeqoa  37437  finxpeq2  37454  finxpreclem6  37463  finxpsuclem  37464  sdclem2  37805  ldualvsub  39277  ldualvsubval  39279  isopos  39302  polfvalN  40026  psubclsetN  40058  docaffvalN  41243  docafvalN  41244  djaffvalN  41255  djafvalN  41256  dihffval  41352  dihfval  41353  dochffval  41471  dochfval  41472  djhffval  41518  djhfval  41519  islpolN  41605  lcdfval  41710  lcdval  41711  lcdvsub  41739  lcdvsubval  41740  mapdffval  41748  mapdfval  41749  hdmap1fval  41918  hdmapfval  41949  hgmapfval  42008  hdmapglem7  42051  hlhilset  42056  aks6d1c1p1  42223  evlselv  42708  0prjspnrel  42748  ismrc  42821  rmxfval  43024  rmyfval  43025  aomclem8  43181  hbt  43250  elmnc  43256  mncn0  43259  aaitgo  43282  clsk1independent  44166  binomcxp  44477  limciccioolb  45748  limcicciooub  45762  ioccncflimc  46010  icocncflimc  46014  dvnprodlem2  46072  dvnprodlem3  46073  dirkercncflem3  46230  fourierdlem32  46264  etransclem32  46391  etransclem44  46403  etransclem46  46405  etransc  46408  ovnsubaddlem1  46695  ovnsubaddlem2  46696  ovnsubadd  46697  hoidmvlelem4  46723  hoidmvlelem5  46724  hspmbl  46754  vonioo  46807  vonicc  46810  afveq12d  47260  iccelpart  47560  nnsum3primesprm  47917  funcringcsetcALTV2lem7  48423  funcringcsetcALTV2lem9  48425  funcringcsetclem7ALTV  48446  funcringcsetclem9ALTV  48448  cofu1a  49222  cofu2a  49223  cofid1  49242  cofid2  49243  uptr2  49349  swapfida  49408  cofuswapf2  49423  fuco21  49464  fuco23  49469  fucoid  49476  opf2  49534  oppfdiag1  49542  oppfdiag  49544  termolmd  49798