Theorem fveq12d 6878

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

Syntax hints:   → wi 4   = wceq 1563  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533

This theorem is referenced by:  nffvd  6883  fvmpopr2d  7562  tfrlem3a  8351  resixpfo  8922  cantnfval  9625  cantnfres  9634  fseqenlem1  9996  fseqenlem2  9997  dfac12lem1  10115  dfac12lem2  10116  dfac12r  10118  hsmexlem2  10399  ttukeylem3  10483  ttukey2g  10488  seq1  14038  expval  14087  lsw  14589  ccatfval  14598  swrdval  14669  splfv2a  14781  revval  14785  relexpsucnnr  15050  relexp1g  15051  seqshft  15110  climshft2  15621  fprodser  15991  imasval  17553  funcid  17915  funcco  17916  funcoppc  17920  funcres  17941  nati  18003  funcestrcsetclem7  18190  funcestrcsetclem9  18192  funcsetcestrclem7  18205  funcsetcestrclem9  18207  evlf2  18262  evlf1  18264  evlfcl  18266  uncf2  18281  hofcl  18303  yonedalem21  18317  yonedalem3a  18318  yonedalem4a  18319  yonedalem4b  18320  yonedalem22  18322  yonedalem3  18324  yonedainv  18325  p0val  18469  p1val  18470  gsumvalx  18722  gsumpropd  18724  gsumval2a  18731  gsumsgrpccat  18887  prdsinvlem  19103  mulgfval  19123  mulgfvalALT  19124  mulgval  19125  mulgnndir  19157  mulgpropd  19170  cntrval  19377  efgsf  19787  efgsval  19789  issrngd  20924  rlmval  21278  chrval  21630  znval  21642  isphl  21735  isphld  21761  phlpropd  21762  cssval  21789  prdsinvgd2  21849  islindf  21919  evlseu  22191  evlval  22208  selvffval  22226  selvval  22228  evls1fval  22436  evl1varpw  22478  madetsumid  22575  madufval  22751  smadiadetr  22789  decpmatval0  22878  chpmatfval  22944  isperf  23265  dfac14  23732  xkohmeo  23929  flffval  24103  fcfval  24147  cnextfval  24176  tsmsval2  24244  tsmspropd  24246  tngngp  24768  tngngp3  24770  isnlm  24789  sranlm  24798  cnncvsabsnegdemo  25281  ovoliunlem1  25618  ovoliunlem2  25619  limcfval  25988  dvfval  26013  dvreslem  26025  dvaddbr  26054  dvmulbr  26055  isuc1p  26255  ismon1p  26257  mon1pid  26268  q1pval  26269  dgreq0  26379  vieta1lem2  26429  vieta1  26430  basellem5  27203  lgsval  27419  lgsneg  27439  seqseq123d  28433  israg  28924  iswlkon  29910  wlkres  29923  wlkp1lem3  29928  wlkp1lem6  29931  isclwlk  30027  iscrct  30044  iscycl  30045  eupth2eucrct  30473  dipfval  30959  prodindf  33090  splfv3  33186  cycpmco2lem5  33358  cycpmco2lem6  33359  idlsrgval  33705  m1pmeq  33787  mplvrpmfgalem  33846  mplvrpmga  33847  mplvrpmmhm  33848  mplvrpmrhm  33849  issply  33863  esplyval  33864  esplyind  33877  vieta  33882  extdgval  33955  fldextrspundgle  33980  minplyval  34007  constrcon  34076  2sqr3minply  34082  lmatfval  34116  lmat22e11  34120  rrhval  34298  xrhval  34320  brae  34543  braew  34544  sitmval  34651  sseqval  34690  fibp1  34703  elprob  34711  signsvtn0  34869  signstfvneq0  34871  signstfveq0  34876  breprexplema  34929  breprexp  34932  circlevma  34941  circlemethhgt  34942  cvmliftlem5  35647  cvmliftlem7  35649  cvmliftlem10  35652  cvmliftlem13  35654  satefv  35772  mclsval  35921  rdgprc0  36149  dfrdg2  36151  bj-finsumval0  37784  rdgeqoa  37871  finxpeq2  37888  finxpreclem6  37897  finxpsuclem  37898  sdclem2  38248  ldualvsub  39786  ldualvsubval  39788  isopos  39811  polfvalN  40535  psubclsetN  40567  docaffvalN  41752  docafvalN  41753  djaffvalN  41764  djafvalN  41765  dihffval  41861  dihfval  41862  dochffval  41980  dochfval  41981  djhffval  42027  djhfval  42028  islpolN  42114  lcdfval  42219  lcdval  42220  lcdvsub  42248  lcdvsubval  42249  mapdffval  42257  mapdfval  42258  hdmap1fval  42427  hdmapfval  42458  hgmapfval  42517  hdmapglem7  42560  hlhilset  42565  aks6d1c1p1  42731  evlselv  43178  0prjspnrel  43216  ismrc  43289  rmxfval  43488  rmyfval  43489  aomclem8  43645  hbt  43714  elmnc  43720  mncn0  43723  aaitgo  43746  clsk1independent  44629  binomcxp  44926  limciccioolb  46196  limcicciooub  46210  ioccncflimc  46458  icocncflimc  46462  dvnprodlem2  46520  dvnprodlem3  46521  dirkercncflem3  46678  fourierdlem32  46712  etransclem32  46839  etransclem44  46851  etransclem46  46853  etransc  46856  ovnsubaddlem1  47143  ovnsubaddlem2  47144  ovnsubadd  47145  hoidmvlelem4  47171  hoidmvlelem5  47172  hspmbl  47202  vonioo  47255  vonicc  47258  afveq12d  47726  iccelpart  48038  nnsum3primesprm  48411  funcringcsetcALTV2lem7  48917  funcringcsetcALTV2lem9  48919  funcringcsetclem7ALTV  48940  funcringcsetclem9ALTV  48942  cofu1a  49724  cofu2a  49725  cofid1  49744  cofid2  49745  uptr2  49851  swapfida  49910  cofuswapf2  49925  fuco21  49966  fuco23  49971  fucoid  49978  opf2  50036  oppfdiag1  50044  oppfdiag  50046  termolmd  50300