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

Theorem fveq12d 5531
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 5527 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5529 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2315 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   ` cfv 5255
This theorem is referenced by:  nffvd  5534  fvsng  5714  resixpfo  6854  cantnfval  7369  cantnfres  7379  fseqenlem1  7651  fseqenlem2  7652  dfac12lem1  7769  dfac12lem2  7770  dfac12r  7772  hsmexlem2  8053  ttukeylem3  8138  ttukey2g  8143  seq1  11059  expval  11106  ccatfval  11428  swrdval  11450  splfv2a  11471  revval  11478  seqshft  11580  climshft2  12056  imasval  13414  funcid  13744  funcco  13745  funcoppc  13749  funcres  13770  nati  13829  evlf2  13992  evlf1  13994  evlfcl  13996  curf1  13999  uncf2  14011  hofcl  14033  yonedalem21  14047  yonedalem3a  14048  yonedalem4a  14049  yonedalem4b  14050  yonedalem22  14052  yonedalem3  14054  yonedainv  14055  p0val  14147  p1val  14148  gsumvalx  14451  gsumpropd  14453  gsumval2a  14459  gsumccat  14464  mulgfval  14568  mulgval  14569  mulgnndir  14589  mulgpropd  14600  prdsinvlem  14603  cntrval  14795  efgsf  15038  efgsval  15040  issrngd  15626  rlmval  15945  chrval  16479  znval  16489  isphl  16532  isphld  16558  phlpropd  16559  cssval  16582  isperf  16882  dfac14  17312  xkohmeo  17506  flffval  17684  fcfval  17728  tsmsval2  17812  tsmspropd  17814  tngngp  18170  isnlm  18186  sranlm  18195  ovoliunlem1  18861  ovoliunlem2  18862  limcfval  19222  dvfval  19247  dvreslem  19259  dvaddbr  19287  dvmulbr  19288  evlseu  19400  evlval  19408  isuc1p  19526  ismon1p  19528  q1pval  19539  dgreq0  19646  vieta1lem2  19691  vieta1  19692  basellem5  20322  lgsval  20539  lgsneg  20558  gxfval  20924  dipfval  21275  cvmliftlem5  23231  cvmliftlem7  23233  cvmliftlem10  23236  cvmliftlem13  23238  rdgprc0  23561  dfrdg2  23563  dffprod  24731  isder  25119  isiso  25237  cinvlem1  25240  isfuna  25246  isntr  25285  sdclem2  25864  ismrc  26188  rmxfval  26401  rmyfval  26402  aomclem8  26571  prdsinvgd2  26620  islindf  26694  hbt  26746  elmnc  26753  mncn0  26756  aaitgo  26779  mdetfval  26899  mon1pid  26936  afveq12d  27408  ldualvsub  28718  ldualvsubval  28720  isopos  28743  polfvalN  29466  psubclsetN  29498  docaffvalN  30684  docafvalN  30685  djaffvalN  30696  djafvalN  30697  dihffval  30793  dihfval  30794  dochffval  30912  dochfval  30913  djhffval  30959  djhfval  30960  islpolN  31046  lcdfval  31151  lcdval  31152  lcdvsub  31180  lcdvsubval  31181  mapdffval  31189  mapdfval  31190  hdmap1fval  31360  hdmapfval  31393  hgmapfval  31452  hdmapglem7  31495  hlhilset  31500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator