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

Theorem fveq12d 5547
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 5543 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5545 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2328 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ` cfv 5271
This theorem is referenced by:  nffvd  5550  fvsng  5730  resixpfo  6870  cantnfval  7385  cantnfres  7395  fseqenlem1  7667  fseqenlem2  7668  dfac12lem1  7785  dfac12lem2  7786  dfac12r  7788  hsmexlem2  8069  ttukeylem3  8154  ttukey2g  8159  seq1  11075  expval  11122  ccatfval  11444  swrdval  11466  splfv2a  11487  revval  11494  seqshft  11596  climshft2  12072  imasval  13430  funcid  13760  funcco  13761  funcoppc  13765  funcres  13786  nati  13845  evlf2  14008  evlf1  14010  evlfcl  14012  curf1  14015  uncf2  14027  hofcl  14049  yonedalem21  14063  yonedalem3a  14064  yonedalem4a  14065  yonedalem4b  14066  yonedalem22  14068  yonedalem3  14070  yonedainv  14071  p0val  14163  p1val  14164  gsumvalx  14467  gsumpropd  14469  gsumval2a  14475  gsumccat  14480  mulgfval  14584  mulgval  14585  mulgnndir  14605  mulgpropd  14616  prdsinvlem  14619  cntrval  14811  efgsf  15054  efgsval  15056  issrngd  15642  rlmval  15961  chrval  16495  znval  16505  isphl  16548  isphld  16574  phlpropd  16575  cssval  16598  isperf  16898  dfac14  17328  xkohmeo  17522  flffval  17700  fcfval  17744  tsmsval2  17828  tsmspropd  17830  tngngp  18186  isnlm  18202  sranlm  18211  ovoliunlem1  18877  ovoliunlem2  18878  limcfval  19238  dvfval  19263  dvreslem  19275  dvaddbr  19303  dvmulbr  19304  evlseu  19416  evlval  19424  isuc1p  19542  ismon1p  19544  q1pval  19555  dgreq0  19662  vieta1lem2  19707  vieta1  19708  basellem5  20338  lgsval  20555  lgsneg  20574  gxfval  20940  dipfval  21291  elprob  23627  cvmliftlem5  23835  cvmliftlem7  23837  cvmliftlem10  23840  cvmliftlem13  23842  rdgprc0  24221  dfrdg2  24223  dffprod  25422  isder  25810  isiso  25928  cinvlem1  25931  isfuna  25937  isntr  25976  sdclem2  26555  ismrc  26879  rmxfval  27092  rmyfval  27093  aomclem8  27262  prdsinvgd2  27311  islindf  27385  hbt  27437  elmnc  27444  mncn0  27447  aaitgo  27470  mdetfval  27590  mon1pid  27627  afveq12d  28101  iswlkon  28332  iscrct  28369  iscycl  28370  ldualvsub  29967  ldualvsubval  29969  isopos  29992  polfvalN  30715  psubclsetN  30747  docaffvalN  31933  docafvalN  31934  djaffvalN  31945  djafvalN  31946  dihffval  32042  dihfval  32043  dochffval  32161  dochfval  32162  djhffval  32208  djhfval  32209  islpolN  32295  lcdfval  32400  lcdval  32401  lcdvsub  32429  lcdvsubval  32430  mapdffval  32438  mapdfval  32439  hdmap1fval  32609  hdmapfval  32642  hgmapfval  32701  hdmapglem7  32744  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator