Theorem fveq12d 6889

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545

This theorem is used by:  nffvd  6894  fvmpopr2d  7579  tfrlem3a  8369  resixpfo  8947  cantnfval  9651  cantnfres  9660  fseqenlem1  10031  fseqenlem2  10032  dfac12lem1  10150  dfac12lem2  10151  dfac12r  10153  hsmexlem2  10433  ttukeylem3  10517  ttukey2g  10522  seq1  14082  expval  14131  lsw  14633  ccatfval  14642  swrdval  14715  splfv2a  14829  revval  14833  relexpsucnnr  15102  relexp1g  15103  seqshft  15162  climshft2  15673  fprodser  16042  imasval  17603  funcid  17965  funcco  17966  funcoppc  17970  funcres  17991  nati  18053  funcestrcsetclem7  18240  funcestrcsetclem9  18242  funcsetcestrclem7  18255  funcsetcestrclem9  18257  evlf2  18312  evlf1  18314  evlfcl  18316  uncf2  18331  hofcl  18353  yonedalem21  18367  yonedalem3a  18368  yonedalem4a  18369  yonedalem4b  18370  yonedalem22  18372  yonedalem3  18374  yonedainv  18375  p0val  18519  p1val  18520  gsumvalx  18784  gsumpropd  18786  gsumval2a  18793  gsumsgrpccat  18955  prdsinvlem  19178  mulgfval  19198  mulgfvalALT  19199  mulgval  19200  mulgnndir  19232  mulgpropd  19245  cntrval  19452  efgsf  19862  efgsval  19864  issrngd  21027  rlmval  21381  chrval  21742  znval  21754  isphl  21847  isphld  21873  phlpropd  21874  cssval  21901  prdsinvgd2  21961  islindf  22031  evlseu  22305  evlval  22322  selvffval  22340  selvval  22342  evls1fval  22550  evl1varpw  22592  madetsumid  22689  madufval  22865  smadiadetr  22903  decpmatval0  22995  chpmatfval  23061  isperf  23382  dfac14  23850  xkohmeo  24047  flffval  24221  fcfval  24265  cnextfval  24294  tsmsval2  24362  tsmspropd  24364  tngngp  24886  tngngp3  24888  isnlm  24907  sranlm  24916  cnncvsabsnegdemo  25399  ovoliunlem1  25736  ovoliunlem2  25737  limcfval  26106  dvfval  26131  dvreslem  26143  dvaddbr  26172  dvmulbr  26173  isuc1p  26373  ismon1p  26375  mon1pid  26386  q1pval  26387  dgreq0  26498  vieta1lem2  26550  vieta1  26551  basellem5  27329  lgsval  27545  lgsneg  27565  seqseq123d  28559  israg  29059  angmgmaddeu1  29266  iswlkon  30123  wlkres  30136  wlkp1lem3  30141  wlkp1lem6  30144  isclwlk  30247  iscrct  30264  iscycl  30265  eupth2eucrct  30705  dipfval  31191  prodindf  33316  splfv3  33406  cycpmco2lem5  33578  cycpmco2lem6  33579  idlsrgval  33921  m1pmeq  34003  mplvrpmfgalem  34062  mplvrpmga  34063  mplvrpmmhm  34064  mplvrpmrhm  34065  issply  34079  esplyval  34080  esplyind  34093  vieta  34098  extdgval  34171  fldextrspundgle  34196  minplyval  34223  constrcon  34292  2sqr3minply  34298  lmatfval  34332  lmat22e11  34336  rrhval  34514  xrhval  34536  brae  34760  braew  34761  sitmval  34868  sseqval  34907  fibp1  34920  elprob  34928  signsvtn0  35086  signstfvneq0  35088  signstfveq0  35093  breprexplema  35146  breprexp  35149  circlevma  35158  circlemethhgt  35159  cvmliftlem5  35876  cvmliftlem7  35878  cvmliftlem10  35881  cvmliftlem13  35883  satefv  36001  mclsval  36150  rdgprc0  36378  dfrdg2  36380  bj-finsumval0  38045  rdgeqoa  38132  finxpeq2  38149  finxpreclem6  38158  finxpsuclem  38159  sdclem2  38500  ldualvsub  40036  ldualvsubval  40038  isopos  40061  polfvalN  40785  psubclsetN  40817  docaffvalN  42002  docafvalN  42003  djaffvalN  42014  djafvalN  42015  dihffval  42111  dihfval  42112  dochffval  42230  dochfval  42231  djhffval  42277  djhfval  42278  islpolN  42364  lcdfval  42469  lcdval  42470  lcdvsub  42498  lcdvsubval  42499  mapdffval  42507  mapdfval  42508  hdmap1fval  42677  hdmapfval  42708  hgmapfval  42767  hdmapglem7  42810  hlhilset  42815  aks6d1c1p1  42981  evlselv  43443  0prjspnrel  43481  ismrc  43554  rmxfval  43753  rmyfval  43754  aomclem8  43910  hbt  43979  elmnc  43985  mncn0  43988  aaitgo  44011  clsk1independent  44894  binomcxp  45189  limciccioolb  46459  limcicciooub  46473  ioccncflimc  46721  icocncflimc  46725  dvnprodlem2  46783  dvnprodlem3  46784  dirkercncflem3  46941  fourierdlem32  46975  etransclem32  47102  etransclem44  47114  etransclem46  47116  etransc  47119  ovnsubaddlem1  47406  ovnsubaddlem2  47407  ovnsubadd  47408  hoidmvlelem4  47434  hoidmvlelem5  47435  hspmbl  47465  vonioo  47518  vonicc  47521  afveq12d  48029  iccelpart  48341  nnsum3primesprm  48714  funcringcsetcALTV2lem7  49219  funcringcsetcALTV2lem9  49221  funcringcsetclem7ALTV  49242  funcringcsetclem9ALTV  49244  cofu1a  50028  cofu2a  50029  cofid1  50048  cofid2  50049  uptr2  50155  swapfida  50214  cofuswapf2  50229  fuco21  50270  fuco23  50275  fucoid  50282  opf2  50340  oppfdiag1  50348  oppfdiag  50350  termolmd  50604