Theorem fveq12d 6841

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500

This theorem is referenced by:  nffvd  6846  fvmpopr2d  7522  tfrlem3a  8309  resixpfo  8877  cantnfval  9580  cantnfres  9589  fseqenlem1  9937  fseqenlem2  9938  dfac12lem1  10057  dfac12lem2  10058  dfac12r  10060  hsmexlem2  10340  ttukeylem3  10424  ttukey2g  10429  seq1  13967  expval  14016  lsw  14517  ccatfval  14526  swrdval  14597  splfv2a  14709  revval  14713  relexpsucnnr  14978  relexp1g  14979  seqshft  15038  climshft2  15535  fprodser  15905  imasval  17466  funcid  17828  funcco  17829  funcoppc  17833  funcres  17854  nati  17916  funcestrcsetclem7  18103  funcestrcsetclem9  18105  funcsetcestrclem7  18118  funcsetcestrclem9  18120  evlf2  18175  evlf1  18177  evlfcl  18179  uncf2  18194  hofcl  18216  yonedalem21  18230  yonedalem3a  18231  yonedalem4a  18232  yonedalem4b  18233  yonedalem22  18235  yonedalem3  18237  yonedainv  18238  p0val  18382  p1val  18383  gsumvalx  18635  gsumpropd  18637  gsumval2a  18644  gsumsgrpccat  18799  prdsinvlem  19016  mulgfval  19036  mulgfvalALT  19037  mulgval  19038  mulgnndir  19070  mulgpropd  19083  cntrval  19285  efgsf  19695  efgsval  19697  issrngd  20823  rlmval  21178  chrval  21513  znval  21525  isphl  21618  isphld  21644  phlpropd  21645  cssval  21672  prdsinvgd2  21732  islindf  21802  evlseu  22071  evlval  22088  selvffval  22109  selvval  22111  evls1fval  22294  evl1varpw  22336  madetsumid  22436  madufval  22612  smadiadetr  22650  decpmatval0  22739  chpmatfval  22805  isperf  23126  dfac14  23593  xkohmeo  23790  flffval  23964  fcfval  24008  cnextfval  24037  tsmsval2  24105  tsmspropd  24107  tngngp  24629  tngngp3  24631  isnlm  24650  sranlm  24659  cnncvsabsnegdemo  25142  ovoliunlem1  25479  ovoliunlem2  25480  limcfval  25849  dvfval  25874  dvreslem  25886  dvaddbr  25915  dvmulbr  25916  isuc1p  26116  ismon1p  26118  mon1pid  26129  q1pval  26130  dgreq0  26240  vieta1lem2  26288  vieta1  26289  basellem5  27062  lgsval  27278  lgsneg  27298  seqseq123d  28292  israg  28779  iswlkon  29739  wlkres  29752  wlkp1lem3  29757  wlkp1lem6  29760  isclwlk  29856  iscrct  29873  iscycl  29874  eupth2eucrct  30302  dipfval  30788  prodindf  32937  splfv3  33033  cycpmco2lem5  33206  cycpmco2lem6  33207  idlsrgval  33578  m1pmeq  33660  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  issply  33720  esplyval  33721  esplyind  33734  vieta  33739  extdgval  33813  fldextrspundgle  33838  minplyval  33865  constrcon  33934  2sqr3minply  33940  lmatfval  33974  lmat22e11  33978  rrhval  34156  xrhval  34178  brae  34401  braew  34402  sitmval  34509  sseqval  34548  fibp1  34561  elprob  34569  signsvtn0  34730  signstfvneq0  34732  signstfveq0  34737  breprexplema  34790  breprexp  34793  circlevma  34802  circlemethhgt  34803  cvmliftlem5  35487  cvmliftlem7  35489  cvmliftlem10  35492  cvmliftlem13  35494  satefv  35612  mclsval  35761  rdgprc0  35989  dfrdg2  35991  bj-finsumval0  37615  rdgeqoa  37700  finxpeq2  37717  finxpreclem6  37726  finxpsuclem  37727  sdclem2  38077  ldualvsub  39615  ldualvsubval  39617  isopos  39640  polfvalN  40364  psubclsetN  40396  docaffvalN  41581  docafvalN  41582  djaffvalN  41593  djafvalN  41594  dihffval  41690  dihfval  41691  dochffval  41809  dochfval  41810  djhffval  41856  djhfval  41857  islpolN  41943  lcdfval  42048  lcdval  42049  lcdvsub  42077  lcdvsubval  42078  mapdffval  42086  mapdfval  42087  hdmap1fval  42256  hdmapfval  42287  hgmapfval  42346  hdmapglem7  42389  hlhilset  42394  aks6d1c1p1  42560  evlselv  43034  0prjspnrel  43074  ismrc  43147  rmxfval  43350  rmyfval  43351  aomclem8  43507  hbt  43576  elmnc  43582  mncn0  43585  aaitgo  43608  clsk1independent  44491  binomcxp  44802  limciccioolb  46069  limcicciooub  46083  ioccncflimc  46331  icocncflimc  46335  dvnprodlem2  46393  dvnprodlem3  46394  dirkercncflem3  46551  fourierdlem32  46585  etransclem32  46712  etransclem44  46724  etransclem46  46726  etransc  46729  ovnsubaddlem1  47016  ovnsubaddlem2  47017  ovnsubadd  47018  hoidmvlelem4  47044  hoidmvlelem5  47045  hspmbl  47075  vonioo  47128  vonicc  47131  afveq12d  47593  iccelpart  47905  nnsum3primesprm  48278  funcringcsetcALTV2lem7  48784  funcringcsetcALTV2lem9  48786  funcringcsetclem7ALTV  48807  funcringcsetclem9ALTV  48809  cofu1a  49581  cofu2a  49582  cofid1  49601  cofid2  49602  uptr2  49708  swapfida  49767  cofuswapf2  49782  fuco21  49823  fuco23  49828  fucoid  49835  opf2  49893  oppfdiag1  49901  oppfdiag  49903  termolmd  50157