Theorem fveq12d 6900

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

Syntax hints:   → wi 4   = wceq 1534  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-iota 6498  df-fv 6554

This theorem is referenced by:  nffvd  6905  fvmpopr2d  7580  wrecseq123OLD  8322  tfrlem3a  8399  resixpfo  8957  cantnfval  9704  cantnfres  9713  fseqenlem1  10060  fseqenlem2  10061  dfac12lem1  10179  dfac12lem2  10180  dfac12r  10182  hsmexlem2  10461  ttukeylem3  10545  ttukey2g  10550  seq1  14028  expval  14077  lsw  14567  ccatfval  14576  swrdval  14646  splfv2a  14759  revval  14763  relexpsucnnr  15025  relexp1g  15026  seqshft  15085  climshft2  15579  fprodser  15946  imasval  17521  funcid  17884  funcco  17885  funcoppc  17889  funcres  17910  nati  17973  funcestrcsetclem7  18165  funcestrcsetclem9  18167  funcsetcestrclem7  18180  funcsetcestrclem9  18182  evlf2  18238  evlf1  18240  evlfcl  18242  uncf2  18257  hofcl  18279  yonedalem21  18293  yonedalem3a  18294  yonedalem4a  18295  yonedalem4b  18296  yonedalem22  18298  yonedalem3  18300  yonedainv  18301  p0val  18447  p1val  18448  gsumvalx  18664  gsumpropd  18666  gsumval2a  18673  gsumsgrpccat  18825  prdsinvlem  19039  mulgfval  19059  mulgfvalALT  19060  mulgval  19061  mulgnndir  19093  mulgpropd  19106  cntrval  19309  efgsf  19723  efgsval  19725  issrngd  20830  rlmval  21173  chrval  21513  znval  21525  isphl  21620  isphld  21646  phlpropd  21647  cssval  21674  prdsinvgd2  21736  islindf  21806  evlseu  22094  evlval  22106  selvffval  22124  selvval  22126  evls1fval  22307  evl1varpw  22349  madetsumid  22451  madufval  22627  smadiadetr  22665  decpmatval0  22754  chpmatfval  22820  isperf  23143  dfac14  23610  xkohmeo  23807  flffval  23981  fcfval  24025  cnextfval  24054  tsmsval2  24122  tsmspropd  24124  tngngp  24659  tngngp3  24661  isnlm  24680  sranlm  24689  cnncvsabsnegdemo  25181  ovoliunlem1  25519  ovoliunlem2  25520  limcfval  25889  dvfval  25914  dvreslem  25926  dvaddbr  25956  dvmulbr  25957  dvmulbrOLD  25958  isuc1p  26165  ismon1p  26167  mon1pid  26178  q1pval  26179  dgreq0  26290  vieta1lem2  26336  vieta1  26337  basellem5  27110  lgsval  27327  lgsneg  27347  seqseq123d  28257  israg  28621  iswlkon  29591  wlkres  29604  wlkp1lem3  29609  wlkp1lem6  29612  isclwlk  29707  iscrct  29724  iscycl  29725  eupth2eucrct  30147  dipfval  30632  splfv3  32825  cycpmco2lem5  33012  cycpmco2lem6  33013  idlsrgval  33384  m1pmeq  33461  extdgval  33549  minplyval  33580  2sqr3minply  33620  lmatfval  33642  lmat22e11  33646  rrhval  33824  xrhval  33846  prodindf  33869  brae  34087  braew  34088  sitmval  34196  sseqval  34235  fibp1  34248  elprob  34256  signsvtn0  34429  signstfvneq0  34431  signstfveq0  34436  breprexplema  34489  breprexp  34492  circlevma  34501  circlemethhgt  34502  cvmliftlem5  35130  cvmliftlem7  35132  cvmliftlem10  35135  cvmliftlem13  35137  satefv  35255  mclsval  35404  rdgprc0  35630  dfrdg2  35632  bj-finsumval0  37005  rdgeqoa  37090  finxpeq2  37107  finxpreclem6  37116  finxpsuclem  37117  sdclem2  37456  ldualvsub  38866  ldualvsubval  38868  isopos  38891  polfvalN  39616  psubclsetN  39648  docaffvalN  40833  docafvalN  40834  djaffvalN  40845  djafvalN  40846  dihffval  40942  dihfval  40943  dochffval  41061  dochfval  41062  djhffval  41108  djhfval  41109  islpolN  41195  lcdfval  41300  lcdval  41301  lcdvsub  41329  lcdvsubval  41330  mapdffval  41338  mapdfval  41339  hdmap1fval  41508  hdmapfval  41539  hgmapfval  41598  hdmapglem7  41641  hlhilset  41646  aks6d1c1p1  41819  evlselv  42277  0prjspnrel  42317  ismrc  42395  rmxfval  42598  rmyfval  42599  aomclem8  42759  hbt  42828  elmnc  42834  mncn0  42837  aaitgo  42860  clsk1independent  43750  binomcxp  44068  limciccioolb  45278  limcicciooub  45294  ioccncflimc  45542  icocncflimc  45546  dvnprodlem2  45604  dvnprodlem3  45605  dirkercncflem3  45762  fourierdlem32  45796  etransclem32  45923  etransclem44  45935  etransclem46  45937  etransc  45940  ovnsubaddlem1  46227  ovnsubaddlem2  46228  ovnsubadd  46229  hoidmvlelem4  46255  hoidmvlelem5  46256  hspmbl  46286  vonioo  46339  vonicc  46342  afveq12d  46782  iccelpart  47041  nnsum3primesprm  47398  funcringcsetcALTV2lem7  47709  funcringcsetcALTV2lem9  47711  funcringcsetclem7ALTV  47732  funcringcsetclem9ALTV  47734