Theorem fveq12d 6865

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  nffvd  6870  fvmpopr2d  7551  tfrlem3a  8345  resixpfo  8909  cantnfval  9621  cantnfres  9630  fseqenlem1  9977  fseqenlem2  9978  dfac12lem1  10097  dfac12lem2  10098  dfac12r  10100  hsmexlem2  10380  ttukeylem3  10464  ttukey2g  10469  seq1  13979  expval  14028  lsw  14529  ccatfval  14538  swrdval  14608  splfv2a  14721  revval  14725  relexpsucnnr  14991  relexp1g  14992  seqshft  15051  climshft2  15548  fprodser  15915  imasval  17474  funcid  17832  funcco  17833  funcoppc  17837  funcres  17858  nati  17920  funcestrcsetclem7  18107  funcestrcsetclem9  18109  funcsetcestrclem7  18122  funcsetcestrclem9  18124  evlf2  18179  evlf1  18181  evlfcl  18183  uncf2  18198  hofcl  18220  yonedalem21  18234  yonedalem3a  18235  yonedalem4a  18236  yonedalem4b  18237  yonedalem22  18239  yonedalem3  18241  yonedainv  18242  p0val  18386  p1val  18387  gsumvalx  18603  gsumpropd  18605  gsumval2a  18612  gsumsgrpccat  18767  prdsinvlem  18981  mulgfval  19001  mulgfvalALT  19002  mulgval  19003  mulgnndir  19035  mulgpropd  19048  cntrval  19251  efgsf  19659  efgsval  19661  issrngd  20764  rlmval  21098  chrval  21433  znval  21445  isphl  21537  isphld  21563  phlpropd  21564  cssval  21591  prdsinvgd2  21651  islindf  21721  evlseu  21990  evlval  22002  selvffval  22020  selvval  22022  evls1fval  22206  evl1varpw  22248  madetsumid  22348  madufval  22524  smadiadetr  22562  decpmatval0  22651  chpmatfval  22717  isperf  23038  dfac14  23505  xkohmeo  23702  flffval  23876  fcfval  23920  cnextfval  23949  tsmsval2  24017  tsmspropd  24019  tngngp  24542  tngngp3  24544  isnlm  24563  sranlm  24572  cnncvsabsnegdemo  25065  ovoliunlem1  25403  ovoliunlem2  25404  limcfval  25773  dvfval  25798  dvreslem  25810  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  isuc1p  26046  ismon1p  26048  mon1pid  26059  q1pval  26060  dgreq0  26171  vieta1lem2  26219  vieta1  26220  basellem5  26995  lgsval  27212  lgsneg  27232  seqseq123d  28180  israg  28624  iswlkon  29585  wlkres  29598  wlkp1lem3  29603  wlkp1lem6  29606  isclwlk  29703  iscrct  29720  iscycl  29721  eupth2eucrct  30146  dipfval  30631  prodindf  32786  splfv3  32880  cycpmco2lem5  33087  cycpmco2lem6  33088  idlsrgval  33474  m1pmeq  33552  extdgval  33649  fldextrspundgle  33673  minplyval  33695  constrcon  33764  2sqr3minply  33770  lmatfval  33804  lmat22e11  33808  rrhval  33986  xrhval  34008  brae  34231  braew  34232  sitmval  34340  sseqval  34379  fibp1  34392  elprob  34400  signsvtn0  34561  signstfvneq0  34563  signstfveq0  34568  breprexplema  34621  breprexp  34624  circlevma  34633  circlemethhgt  34634  cvmliftlem5  35276  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem13  35283  satefv  35401  mclsval  35550  rdgprc0  35781  dfrdg2  35783  bj-finsumval0  37273  rdgeqoa  37358  finxpeq2  37375  finxpreclem6  37384  finxpsuclem  37385  sdclem2  37736  ldualvsub  39148  ldualvsubval  39150  isopos  39173  polfvalN  39898  psubclsetN  39930  docaffvalN  41115  docafvalN  41116  djaffvalN  41127  djafvalN  41128  dihffval  41224  dihfval  41225  dochffval  41343  dochfval  41344  djhffval  41390  djhfval  41391  islpolN  41477  lcdfval  41582  lcdval  41583  lcdvsub  41611  lcdvsubval  41612  mapdffval  41620  mapdfval  41621  hdmap1fval  41790  hdmapfval  41821  hgmapfval  41880  hdmapglem7  41923  hlhilset  41928  aks6d1c1p1  42095  evlselv  42575  0prjspnrel  42615  ismrc  42689  rmxfval  42892  rmyfval  42893  aomclem8  43050  hbt  43119  elmnc  43125  mncn0  43128  aaitgo  43151  clsk1independent  44035  binomcxp  44346  limciccioolb  45619  limcicciooub  45635  ioccncflimc  45883  icocncflimc  45887  dvnprodlem2  45945  dvnprodlem3  45946  dirkercncflem3  46103  fourierdlem32  46137  etransclem32  46264  etransclem44  46276  etransclem46  46278  etransc  46281  ovnsubaddlem1  46568  ovnsubaddlem2  46569  ovnsubadd  46570  hoidmvlelem4  46596  hoidmvlelem5  46597  hspmbl  46627  vonioo  46680  vonicc  46683  afveq12d  47134  iccelpart  47434  nnsum3primesprm  47791  funcringcsetcALTV2lem7  48284  funcringcsetcALTV2lem9  48286  funcringcsetclem7ALTV  48307  funcringcsetclem9ALTV  48309  cofu1a  49083  cofu2a  49084  cofid1  49103  cofid2  49104  uptr2  49210  swapfida  49269  cofuswapf2  49284  fuco21  49325  fuco23  49330  fucoid  49337  opf2  49395  oppfdiag1  49403  oppfdiag  49405  termolmd  49659