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

Theorem fveq12d 5804
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 5800 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5802 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2495 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   ` cfv 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533
This theorem is referenced by:  nffvd  5807  fvsng  6020  tfrlem3a  6945  resixpfo  7410  cantnfval  7986  cantnfres  7995  cantnfvalOLD  8016  fseqenlem1  8304  fseqenlem2  8305  dfac12lem1  8422  dfac12lem2  8423  dfac12r  8425  hsmexlem2  8706  ttukeylem3  8790  ttukey2g  8795  seq1  11935  expval  11983  lsw  12383  ccatfval  12390  swrdval  12430  splfv2a  12515  revval  12517  seqshft  12691  climshft2  13177  imasval  14567  funcid  14898  funcco  14899  funcoppc  14903  funcres  14924  nati  14983  evlf2  15146  evlf1  15148  evlfcl  15150  uncf2  15165  hofcl  15187  yonedalem21  15201  yonedalem3a  15202  yonedalem4a  15203  yonedalem4b  15204  yonedalem22  15206  yonedalem3  15208  yonedainv  15209  p0val  15329  p1val  15330  gsumvalx  15620  gsumpropd  15622  gsumval2a  15630  gsumccat  15637  mulgfval  15746  mulgval  15747  mulgnndir  15767  mulgpropd  15778  prdsinvlem  15781  cntrval  15955  efgsf  16346  efgsval  16348  issrngd  17068  rlmval  17394  evlseu  17725  evlval  17733  evls1fval  17878  evl1varpw  17919  chrval  18080  znval  18090  isphl  18181  isphld  18207  phlpropd  18208  cssval  18231  prdsinvgd2  18291  islindf  18365  madetsumid  18472  madufval  18574  smadiadetr  18612  isperf  18886  dfac14  19322  xkohmeo  19519  flffval  19693  fcfval  19737  cnextfval  19765  tsmsval2  19831  tsmspropd  19833  tngngp  20371  isnlm  20387  sranlm  20396  rrxmval  21035  ovoliunlem1  21116  ovoliunlem2  21117  limcfval  21479  dvfval  21504  dvreslem  21516  dvaddbr  21544  dvmulbr  21545  isuc1p  21744  ismon1p  21746  q1pval  21757  dgreq0  21864  vieta1lem2  21909  vieta1  21910  basellem5  22554  lgsval  22771  lgsneg  22790  istrkg2ld  23054  israg  23233  iswlkon  23581  iscrct  23661  iscycl  23662  gxfval  23895  dipfval  24248  rrhval  26569  xrhval  26588  brae  26800  braew  26801  sitmval  26877  sseqval  26914  fibp1  26927  elprob  26935  signsvtn0  27114  signstfvneq0  27116  signstfveq0  27121  signsvvfval  27122  cvmliftlem5  27321  cvmliftlem7  27323  cvmliftlem10  27326  cvmliftlem13  27328  fprodser  27605  rdgprc0  27750  dfrdg2  27752  wrecseq123  27861  sdclem2  28785  ismrc  29184  rmxfval  29392  rmyfval  29393  aomclem8  29561  hbt  29633  elmnc  29640  mncn0  29643  aaitgo  29666  mon1pid  29720  afveq12d  30186  isclwlk0  30566  decpmatval0  31237  cpmatfval  31300  bj-finsumval0  32906  ldualvsub  33123  ldualvsubval  33125  isopos  33148  polfvalN  33871  psubclsetN  33903  docaffvalN  35089  docafvalN  35090  djaffvalN  35101  djafvalN  35102  dihffval  35198  dihfval  35199  dochffval  35317  dochfval  35318  djhffval  35364  djhfval  35365  islpolN  35451  lcdfval  35556  lcdval  35557  lcdvsub  35585  lcdvsubval  35586  mapdffval  35594  mapdfval  35595  hdmap1fval  35765  hdmapfval  35798  hgmapfval  35857  hdmapglem7  35900  hlhilset  35905
  Copyright terms: Public domain W3C validator