Theorem fveq12d 6868

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

Syntax hints:   → wi 4   = wceq 1559  ‘cfv 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6471  df-fv 6523

This theorem is referenced by:  nffvd  6873  fvmpopr2d  7552  tfrlem3a  8340  resixpfo  8911  cantnfval  9616  cantnfres  9625  fseqenlem1  9973  fseqenlem2  9974  dfac12lem1  10093  dfac12lem2  10094  dfac12r  10096  hsmexlem2  10377  ttukeylem3  10461  ttukey2g  10466  seq1  14020  expval  14069  lsw  14570  ccatfval  14579  swrdval  14650  splfv2a  14762  revval  14766  relexpsucnnr  15031  relexp1g  15032  seqshft  15091  climshft2  15599  fprodser  15969  imasval  17531  funcid  17893  funcco  17894  funcoppc  17898  funcres  17919  nati  17981  funcestrcsetclem7  18168  funcestrcsetclem9  18170  funcsetcestrclem7  18183  funcsetcestrclem9  18185  evlf2  18240  evlf1  18242  evlfcl  18244  uncf2  18259  hofcl  18281  yonedalem21  18295  yonedalem3a  18296  yonedalem4a  18297  yonedalem4b  18298  yonedalem22  18300  yonedalem3  18302  yonedainv  18303  p0val  18447  p1val  18448  gsumvalx  18700  gsumpropd  18702  gsumval2a  18709  gsumsgrpccat  18864  prdsinvlem  19081  mulgfval  19101  mulgfvalALT  19102  mulgval  19103  mulgnndir  19135  mulgpropd  19148  cntrval  19349  efgsf  19759  efgsval  19761  issrngd  20891  rlmval  21245  chrval  21562  znval  21574  isphl  21667  isphld  21693  phlpropd  21694  cssval  21721  prdsinvgd2  21781  islindf  21851  evlseu  22123  evlval  22140  selvffval  22158  selvval  22160  evls1fval  22369  evl1varpw  22411  madetsumid  22508  madufval  22684  smadiadetr  22722  decpmatval0  22811  chpmatfval  22877  isperf  23198  dfac14  23665  xkohmeo  23862  flffval  24036  fcfval  24080  cnextfval  24109  tsmsval2  24177  tsmspropd  24179  tngngp  24701  tngngp3  24703  isnlm  24722  sranlm  24731  cnncvsabsnegdemo  25214  ovoliunlem1  25551  ovoliunlem2  25552  limcfval  25921  dvfval  25946  dvreslem  25958  dvaddbr  25987  dvmulbr  25988  isuc1p  26188  ismon1p  26190  mon1pid  26201  q1pval  26202  dgreq0  26312  vieta1lem2  26362  vieta1  26363  basellem5  27136  lgsval  27352  lgsneg  27372  seqseq123d  28366  israg  28853  iswlkon  29812  wlkres  29825  wlkp1lem3  29830  wlkp1lem6  29833  isclwlk  29929  iscrct  29946  iscycl  29947  eupth2eucrct  30375  dipfval  30861  prodindf  33000  splfv3  33096  cycpmco2lem5  33270  cycpmco2lem6  33271  idlsrgval  33659  m1pmeq  33741  mplvrpmfgalem  33801  mplvrpmga  33802  mplvrpmmhm  33803  mplvrpmrhm  33804  issply  33818  esplyval  33819  esplyind  33832  vieta  33837  extdgval  33910  fldextrspundgle  33935  minplyval  33962  constrcon  34031  2sqr3minply  34037  lmatfval  34071  lmat22e11  34075  rrhval  34253  xrhval  34275  brae  34498  braew  34499  sitmval  34606  sseqval  34645  fibp1  34658  elprob  34666  signsvtn0  34824  signstfvneq0  34826  signstfveq0  34831  breprexplema  34884  breprexp  34887  circlevma  34896  circlemethhgt  34897  cvmliftlem5  35599  cvmliftlem7  35601  cvmliftlem10  35604  cvmliftlem13  35606  satefv  35724  mclsval  35873  rdgprc0  36101  dfrdg2  36103  bj-finsumval0  37737  rdgeqoa  37824  finxpeq2  37841  finxpreclem6  37850  finxpsuclem  37851  sdclem2  38201  ldualvsub  39739  ldualvsubval  39741  isopos  39764  polfvalN  40488  psubclsetN  40520  docaffvalN  41705  docafvalN  41706  djaffvalN  41717  djafvalN  41718  dihffval  41814  dihfval  41815  dochffval  41933  dochfval  41934  djhffval  41980  djhfval  41981  islpolN  42067  lcdfval  42172  lcdval  42173  lcdvsub  42201  lcdvsubval  42202  mapdffval  42210  mapdfval  42211  hdmap1fval  42380  hdmapfval  42411  hgmapfval  42470  hdmapglem7  42513  hlhilset  42518  aks6d1c1p1  42684  evlselv  43131  0prjspnrel  43169  ismrc  43242  rmxfval  43441  rmyfval  43442  aomclem8  43598  hbt  43667  elmnc  43673  mncn0  43676  aaitgo  43699  clsk1independent  44582  binomcxp  44893  limciccioolb  46157  limcicciooub  46171  ioccncflimc  46419  icocncflimc  46423  dvnprodlem2  46481  dvnprodlem3  46482  dirkercncflem3  46639  fourierdlem32  46673  etransclem32  46800  etransclem44  46812  etransclem46  46814  etransc  46817  ovnsubaddlem1  47104  ovnsubaddlem2  47105  ovnsubadd  47106  hoidmvlelem4  47132  hoidmvlelem5  47133  hspmbl  47163  vonioo  47216  vonicc  47219  afveq12d  47687  iccelpart  47999  nnsum3primesprm  48372  funcringcsetcALTV2lem7  48878  funcringcsetcALTV2lem9  48880  funcringcsetclem7ALTV  48901  funcringcsetclem9ALTV  48903  cofu1a  49675  cofu2a  49676  cofid1  49695  cofid2  49696  uptr2  49802  swapfida  49861  cofuswapf2  49876  fuco21  49917  fuco23  49922  fucoid  49929  opf2  49987  oppfdiag1  49995  oppfdiag  49997  termolmd  50251