MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fveq12d Structured version   Unicode version

Theorem fveq12d 5685
Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
fveq12d.1  |-  ( ph  ->  F  =  G )
fveq12d.2  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
fveq12d  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )

Proof of Theorem fveq12d
StepHypRef Expression
1 fveq12d.1 . . 3  |-  ( ph  ->  F  =  G )
21fveq1d 5681 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5683 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2465 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414
This theorem is referenced by:  nffvd  5688  fvsng  5899  tfrlem3a  6822  resixpfo  7289  cantnfval  7864  cantnfres  7873  cantnfvalOLD  7894  fseqenlem1  8182  fseqenlem2  8183  dfac12lem1  8300  dfac12lem2  8301  dfac12r  8303  hsmexlem2  8584  ttukeylem3  8668  ttukey2g  8673  seq1  11803  expval  11851  lsw  12250  ccatfval  12257  swrdval  12297  splfv2a  12382  revval  12384  seqshft  12558  climshft2  13044  imasval  14432  funcid  14763  funcco  14764  funcoppc  14768  funcres  14789  nati  14848  evlf2  15011  evlf1  15013  evlfcl  15015  uncf2  15030  hofcl  15052  yonedalem21  15066  yonedalem3a  15067  yonedalem4a  15068  yonedalem4b  15069  yonedalem22  15071  yonedalem3  15073  yonedainv  15074  p0val  15194  p1val  15195  gsumvalx  15484  gsumpropd  15486  gsumval2a  15492  gsumccat  15499  mulgfval  15608  mulgval  15609  mulgnndir  15629  mulgpropd  15640  prdsinvlem  15643  cntrval  15817  efgsf  16206  efgsval  16208  issrngd  16870  rlmval  17194  chrval  17798  znval  17808  isphl  17899  isphld  17925  phlpropd  17926  cssval  17949  prdsinvgd2  18009  islindf  18083  madetsumid  18188  madufval  18285  smadiadetr  18323  isperf  18597  dfac14  19033  xkohmeo  19230  flffval  19404  fcfval  19448  cnextfval  19476  tsmsval2  19542  tsmspropd  19544  tngngp  20082  isnlm  20098  sranlm  20107  rrxmval  20746  ovoliunlem1  20827  ovoliunlem2  20828  limcfval  21189  dvfval  21214  dvreslem  21226  dvaddbr  21254  dvmulbr  21255  evlseu  21368  evlval  21376  isuc1p  21497  ismon1p  21499  q1pval  21510  dgreq0  21617  vieta1lem2  21662  vieta1  21663  basellem5  22307  lgsval  22524  lgsneg  22543  iswlkon  23253  iscrct  23333  iscycl  23334  gxfval  23567  dipfval  23920  rrhval  26279  xrhval  26298  brae  26511  braew  26512  sitmval  26582  sseqval  26619  fibp1  26632  elprob  26640  signsvtn0  26819  signstfvneq0  26821  signstfveq0  26826  signsvvfval  26827  cvmliftlem5  27026  cvmliftlem7  27028  cvmliftlem10  27031  cvmliftlem13  27033  fprodser  27309  rdgprc0  27454  dfrdg2  27456  wrecseq123  27565  sdclem2  28482  ismrc  28882  rmxfval  29090  rmyfval  29091  aomclem8  29259  hbt  29331  elmnc  29338  mncn0  29341  aaitgo  29364  mon1pid  29418  afveq12d  29885  isclwlk0  30265  bj-finsumval0  32159  ldualvsub  32373  ldualvsubval  32375  isopos  32398  polfvalN  33121  psubclsetN  33153  docaffvalN  34339  docafvalN  34340  djaffvalN  34351  djafvalN  34352  dihffval  34448  dihfval  34449  dochffval  34567  dochfval  34568  djhffval  34614  djhfval  34615  islpolN  34701  lcdfval  34806  lcdval  34807  lcdvsub  34835  lcdvsubval  34836  mapdffval  34844  mapdfval  34845  hdmap1fval  35015  hdmapfval  35048  hgmapfval  35107  hdmapglem7  35150  hlhilset  35155
  Copyright terms: Public domain W3C validator