Theorem fveq12d 6913

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

Syntax hints:   → wi 4   = wceq 1536  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  nffvd  6918  fvmpopr2d  7594  wrecseq123OLD  8338  tfrlem3a  8415  resixpfo  8974  cantnfval  9705  cantnfres  9714  fseqenlem1  10061  fseqenlem2  10062  dfac12lem1  10181  dfac12lem2  10182  dfac12r  10184  hsmexlem2  10464  ttukeylem3  10548  ttukey2g  10553  seq1  14051  expval  14100  lsw  14598  ccatfval  14607  swrdval  14677  splfv2a  14790  revval  14794  relexpsucnnr  15060  relexp1g  15061  seqshft  15120  climshft2  15614  fprodser  15981  imasval  17557  funcid  17920  funcco  17921  funcoppc  17925  funcres  17946  nati  18009  funcestrcsetclem7  18201  funcestrcsetclem9  18203  funcsetcestrclem7  18216  funcsetcestrclem9  18218  evlf2  18274  evlf1  18276  evlfcl  18278  uncf2  18293  hofcl  18315  yonedalem21  18329  yonedalem3a  18330  yonedalem4a  18331  yonedalem4b  18332  yonedalem22  18334  yonedalem3  18336  yonedainv  18337  p0val  18484  p1val  18485  gsumvalx  18701  gsumpropd  18703  gsumval2a  18710  gsumsgrpccat  18865  prdsinvlem  19079  mulgfval  19099  mulgfvalALT  19100  mulgval  19101  mulgnndir  19133  mulgpropd  19146  cntrval  19349  efgsf  19761  efgsval  19763  issrngd  20872  rlmval  21215  chrval  21555  znval  21567  isphl  21663  isphld  21689  phlpropd  21690  cssval  21717  prdsinvgd2  21779  islindf  21849  evlseu  22124  evlval  22136  selvffval  22154  selvval  22156  evls1fval  22338  evl1varpw  22380  madetsumid  22482  madufval  22658  smadiadetr  22696  decpmatval0  22785  chpmatfval  22851  isperf  23174  dfac14  23641  xkohmeo  23838  flffval  24012  fcfval  24056  cnextfval  24085  tsmsval2  24153  tsmspropd  24155  tngngp  24690  tngngp3  24692  isnlm  24711  sranlm  24720  cnncvsabsnegdemo  25212  ovoliunlem1  25550  ovoliunlem2  25551  limcfval  25921  dvfval  25946  dvreslem  25958  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  isuc1p  26194  ismon1p  26196  mon1pid  26207  q1pval  26208  dgreq0  26319  vieta1lem2  26367  vieta1  26368  basellem5  27142  lgsval  27359  lgsneg  27379  seqseq123d  28306  israg  28719  iswlkon  29689  wlkres  29702  wlkp1lem3  29707  wlkp1lem6  29710  isclwlk  29805  iscrct  29822  iscycl  29823  eupth2eucrct  30245  dipfval  30730  splfv3  32927  cycpmco2lem5  33132  cycpmco2lem6  33133  idlsrgval  33510  m1pmeq  33587  extdgval  33681  minplyval  33712  2sqr3minply  33752  lmatfval  33774  lmat22e11  33778  rrhval  33958  xrhval  33980  prodindf  34003  brae  34221  braew  34222  sitmval  34330  sseqval  34369  fibp1  34382  elprob  34390  signsvtn0  34563  signstfvneq0  34565  signstfveq0  34570  breprexplema  34623  breprexp  34626  circlevma  34635  circlemethhgt  34636  cvmliftlem5  35273  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem13  35280  satefv  35398  mclsval  35547  rdgprc0  35774  dfrdg2  35776  bj-finsumval0  37267  rdgeqoa  37352  finxpeq2  37369  finxpreclem6  37378  finxpsuclem  37379  sdclem2  37728  ldualvsub  39136  ldualvsubval  39138  isopos  39161  polfvalN  39886  psubclsetN  39918  docaffvalN  41103  docafvalN  41104  djaffvalN  41115  djafvalN  41116  dihffval  41212  dihfval  41213  dochffval  41331  dochfval  41332  djhffval  41378  djhfval  41379  islpolN  41465  lcdfval  41570  lcdval  41571  lcdvsub  41599  lcdvsubval  41600  mapdffval  41608  mapdfval  41609  hdmap1fval  41778  hdmapfval  41809  hgmapfval  41868  hdmapglem7  41911  hlhilset  41916  aks6d1c1p1  42088  evlselv  42573  0prjspnrel  42613  ismrc  42688  rmxfval  42891  rmyfval  42892  aomclem8  43049  hbt  43118  elmnc  43124  mncn0  43127  aaitgo  43150  clsk1independent  44035  binomcxp  44352  limciccioolb  45576  limcicciooub  45592  ioccncflimc  45840  icocncflimc  45844  dvnprodlem2  45902  dvnprodlem3  45903  dirkercncflem3  46060  fourierdlem32  46094  etransclem32  46221  etransclem44  46233  etransclem46  46235  etransc  46238  ovnsubaddlem1  46525  ovnsubaddlem2  46526  ovnsubadd  46527  hoidmvlelem4  46553  hoidmvlelem5  46554  hspmbl  46584  vonioo  46637  vonicc  46640  afveq12d  47082  iccelpart  47357  nnsum3primesprm  47714  funcringcsetcALTV2lem7  48139  funcringcsetcALTV2lem9  48141  funcringcsetclem7ALTV  48162  funcringcsetclem9ALTV  48164