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

Theorem fveq12d 5872
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 5868 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5870 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2508 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596
This theorem is referenced by:  nffvd  5875  fvsng  6095  tfrlem3a  7046  resixpfo  7507  cantnfval  8087  cantnfres  8096  cantnfvalOLD  8117  fseqenlem1  8405  fseqenlem2  8406  dfac12lem1  8523  dfac12lem2  8524  dfac12r  8526  hsmexlem2  8807  ttukeylem3  8891  ttukey2g  8896  seq1  12088  expval  12136  lsw  12550  ccatfval  12557  swrdval  12607  splfv2a  12695  revval  12697  seqshft  12881  climshft2  13368  imasval  14766  funcid  15097  funcco  15098  funcoppc  15102  funcres  15123  nati  15182  evlf2  15345  evlf1  15347  evlfcl  15349  uncf2  15364  hofcl  15386  yonedalem21  15400  yonedalem3a  15401  yonedalem4a  15402  yonedalem4b  15403  yonedalem22  15405  yonedalem3  15407  yonedainv  15408  p0val  15528  p1val  15529  gsumvalx  15824  gsumpropd  15826  gsumval2a  15834  gsumccat  15841  mulgfval  15953  mulgval  15954  mulgnndir  15974  mulgpropd  15985  prdsinvlem  15988  cntrval  16162  efgsf  16553  efgsval  16555  issrngd  17310  rlmval  17637  evlseu  17984  evlval  17992  evls1fval  18155  evl1varpw  18196  chrval  18357  znval  18367  isphl  18458  isphld  18484  phlpropd  18485  cssval  18508  prdsinvgd2  18568  islindf  18642  madetsumid  18758  madufval  18934  smadiadetr  18972  decpmatval0  19060  chpmatfval  19126  isperf  19446  dfac14  19882  xkohmeo  20079  flffval  20253  fcfval  20297  cnextfval  20325  tsmsval2  20391  tsmspropd  20393  tngngp  20931  isnlm  20947  sranlm  20956  rrxmval  21595  ovoliunlem1  21676  ovoliunlem2  21677  limcfval  22039  dvfval  22064  dvreslem  22076  dvaddbr  22104  dvmulbr  22105  isuc1p  22304  ismon1p  22306  q1pval  22317  dgreq0  22424  vieta1lem2  22469  vieta1  22470  basellem5  23114  lgsval  23331  lgsneg  23350  istrkg2ld  23614  israg  23810  iswlkon  24238  iscrct  24328  iscycl  24329  isclwlk0  24458  gxfval  24963  dipfval  25316  rrhval  27641  xrhval  27660  brae  27881  braew  27882  sitmval  27958  sseqval  27995  fibp1  28008  elprob  28016  signsvtn0  28195  signstfvneq0  28197  signstfveq0  28202  signsvvfval  28203  cvmliftlem5  28402  cvmliftlem7  28404  cvmliftlem10  28407  cvmliftlem13  28409  fprodser  28686  rdgprc0  28831  dfrdg2  28833  wrecseq123  28942  sdclem2  29866  ismrc  30265  rmxfval  30472  rmyfval  30473  aomclem8  30639  hbt  30711  elmnc  30718  mncn0  30721  aaitgo  30744  mon1pid  30798  limciccioolb  31191  limcicciooub  31207  cncfshift  31240  cncfperiod  31245  ioccncflimc  31252  icocncflimc  31256  cncfiooicclem1  31260  dirkercncflem3  31433  fourierdlem32  31467  afveq12d  31713  bj-finsumval0  33753  ldualvsub  33970  ldualvsubval  33972  isopos  33995  polfvalN  34718  psubclsetN  34750  docaffvalN  35936  docafvalN  35937  djaffvalN  35948  djafvalN  35949  dihffval  36045  dihfval  36046  dochffval  36164  dochfval  36165  djhffval  36211  djhfval  36212  islpolN  36298  lcdfval  36403  lcdval  36404  lcdvsub  36432  lcdvsubval  36433  mapdffval  36441  mapdfval  36442  hdmap1fval  36612  hdmapfval  36645  hgmapfval  36704  hdmapglem7  36747  hlhilset  36752
  Copyright terms: Public domain W3C validator