Theorem fveq12d 6775

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438

This theorem is referenced by:  nffvd  6780  fvmpopr2d  7425  wrecseq123OLD  8115  tfrlem3a  8192  resixpfo  8698  cantnfval  9387  cantnfres  9396  fseqenlem1  9764  fseqenlem2  9765  dfac12lem1  9883  dfac12lem2  9884  dfac12r  9886  hsmexlem2  10167  ttukeylem3  10251  ttukey2g  10256  seq1  13715  expval  13765  lsw  14248  ccatfval  14257  swrdval  14337  splfv2a  14450  revval  14454  relexpsucnnr  14717  relexp1g  14718  seqshft  14777  climshft2  15272  fprodser  15640  imasval  17203  funcid  17566  funcco  17567  funcoppc  17571  funcres  17592  nati  17652  funcestrcsetclem7  17844  funcestrcsetclem9  17846  funcsetcestrclem7  17859  funcsetcestrclem9  17861  evlf2  17917  evlf1  17919  evlfcl  17921  uncf2  17936  hofcl  17958  yonedalem21  17972  yonedalem3a  17973  yonedalem4a  17974  yonedalem4b  17975  yonedalem22  17977  yonedalem3  17979  yonedainv  17980  p0val  18126  p1val  18127  gsumvalx  18341  gsumpropd  18343  gsumval2a  18350  gsumsgrpccat  18459  gsumccatOLD  18460  prdsinvlem  18665  mulgfval  18683  mulgfvalALT  18684  mulgval  18685  mulgnndir  18713  mulgpropd  18726  cntrval  18906  efgsf  19316  efgsval  19318  issrngd  20102  rlmval  20442  chrval  20710  znval  20720  isphl  20814  isphld  20840  phlpropd  20841  cssval  20868  prdsinvgd2  20930  islindf  21000  evlseu  21274  evlval  21286  selvffval  21307  selvval  21309  evls1fval  21466  evl1varpw  21508  madetsumid  21591  madufval  21767  smadiadetr  21805  decpmatval0  21894  chpmatfval  21960  isperf  22283  dfac14  22750  xkohmeo  22947  flffval  23121  fcfval  23165  cnextfval  23194  tsmsval2  23262  tsmspropd  23264  tngngp  23799  tngngp3  23801  isnlm  23820  sranlm  23829  cnncvsabsnegdemo  24310  ovoliunlem1  24647  ovoliunlem2  24648  limcfval  25017  dvfval  25042  dvreslem  25054  dvaddbr  25083  dvmulbr  25084  isuc1p  25286  ismon1p  25288  q1pval  25299  dgreq0  25407  vieta1lem2  25452  vieta1  25453  basellem5  26215  lgsval  26430  lgsneg  26450  israg  27039  iswlkon  28005  wlkres  28018  wlkp1lem3  28023  wlkp1lem6  28026  isclwlk  28120  iscrct  28137  iscycl  28138  eupth2eucrct  28560  dipfval  29043  splfv3  31209  cycpmco2lem5  31376  cycpmco2lem6  31377  idlsrgval  31627  extdgval  31708  lmatfval  31743  lmat22e11  31747  rrhval  31925  xrhval  31947  prodindf  31970  brae  32188  braew  32189  sitmval  32295  sseqval  32334  fibp1  32347  elprob  32355  signsvtn0  32528  signstfvneq0  32530  signstfveq0  32535  breprexplema  32589  breprexp  32592  circlevma  32601  circlemethhgt  32602  cvmliftlem5  33230  cvmliftlem7  33232  cvmliftlem10  33235  cvmliftlem13  33237  satefv  33355  mclsval  33504  rdgprc0  33748  dfrdg2  33750  bj-finsumval0  35435  rdgeqoa  35520  finxpeq2  35537  finxpreclem6  35546  finxpsuclem  35547  sdclem2  35879  ldualvsub  37148  ldualvsubval  37150  isopos  37173  polfvalN  37897  psubclsetN  37929  docaffvalN  39114  docafvalN  39115  djaffvalN  39126  djafvalN  39127  dihffval  39223  dihfval  39224  dochffval  39342  dochfval  39343  djhffval  39389  djhfval  39390  islpolN  39476  lcdfval  39581  lcdval  39582  lcdvsub  39610  lcdvsubval  39611  mapdffval  39619  mapdfval  39620  hdmap1fval  39789  hdmapfval  39820  hgmapfval  39879  hdmapglem7  39922  hlhilset  39927  0prjspnrel  40444  ismrc  40503  rmxfval  40706  rmyfval  40707  aomclem8  40866  hbt  40935  elmnc  40941  mncn0  40944  aaitgo  40967  mon1pid  41010  clsk1independent  41609  binomcxp  41928  limciccioolb  43116  limcicciooub  43132  ioccncflimc  43380  icocncflimc  43384  dvnprodlem2  43442  dvnprodlem3  43443  dirkercncflem3  43600  fourierdlem32  43634  etransclem32  43761  etransclem44  43773  etransclem46  43775  etransc  43778  ovnsubaddlem1  44062  ovnsubaddlem2  44063  ovnsubadd  44064  hoidmvlelem4  44090  hoidmvlelem5  44091  hspmbl  44121  vonioo  44174  vonicc  44177  afveq12d  44576  iccelpart  44837  nnsum3primesprm  45194  isomgreqve  45229  funcringcsetcALTV2lem7  45552  funcringcsetcALTV2lem9  45554  funcringcsetclem7ALTV  45575  funcringcsetclem9ALTV  45577