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

Theorem fveq12d 5693
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 5689 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5691 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2436 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ` cfv 5413
This theorem is referenced by:  nffvd  5696  fvsng  5886  resixpfo  7059  cantnfval  7579  cantnfres  7589  fseqenlem1  7861  fseqenlem2  7862  dfac12lem1  7979  dfac12lem2  7980  dfac12r  7982  hsmexlem2  8263  ttukeylem3  8347  ttukey2g  8352  seq1  11291  expval  11339  ccatfval  11697  swrdval  11719  splfv2a  11740  revval  11747  seqshft  11855  climshft2  12331  imasval  13692  funcid  14022  funcco  14023  funcoppc  14027  funcres  14048  nati  14107  evlf2  14270  evlf1  14272  evlfcl  14274  uncf2  14289  hofcl  14311  yonedalem21  14325  yonedalem3a  14326  yonedalem4a  14327  yonedalem4b  14328  yonedalem22  14330  yonedalem3  14332  yonedainv  14333  p0val  14425  p1val  14426  gsumvalx  14729  gsumpropd  14731  gsumval2a  14737  gsumccat  14742  mulgfval  14846  mulgval  14847  mulgnndir  14867  mulgpropd  14878  prdsinvlem  14881  cntrval  15073  efgsf  15316  efgsval  15318  issrngd  15904  rlmval  16219  chrval  16761  znval  16771  isphl  16814  isphld  16840  phlpropd  16841  cssval  16864  isperf  17169  dfac14  17603  xkohmeo  17800  flffval  17974  fcfval  18018  cnextfval  18046  tsmsval2  18112  tsmspropd  18114  tngngp  18648  isnlm  18664  sranlm  18673  ovoliunlem1  19351  ovoliunlem2  19352  limcfval  19712  dvfval  19737  dvreslem  19749  dvaddbr  19777  dvmulbr  19778  evlseu  19890  evlval  19898  isuc1p  20016  ismon1p  20018  q1pval  20029  dgreq0  20136  vieta1lem2  20181  vieta1  20182  basellem5  20820  lgsval  21037  lgsneg  21056  iswlkon  21484  iscrct  21564  iscycl  21565  gxfval  21798  dipfval  22151  rrhval  24332  xrhval  24337  brae  24545  braew  24546  sitmval  24614  elprob  24620  cvmliftlem5  24929  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem13  24936  fprodser  25228  rdgprc0  25364  dfrdg2  25366  sdclem2  26336  ismrc  26645  rmxfval  26857  rmyfval  26858  aomclem8  27027  prdsinvgd2  27076  islindf  27150  hbt  27202  elmnc  27209  mncn0  27212  aaitgo  27235  mdetfval  27355  mon1pid  27392  afveq12d  27864  ldualvsub  29638  ldualvsubval  29640  isopos  29663  polfvalN  30386  psubclsetN  30418  docaffvalN  31604  docafvalN  31605  djaffvalN  31616  djafvalN  31617  dihffval  31713  dihfval  31714  dochffval  31832  dochfval  31833  djhffval  31879  djhfval  31880  islpolN  31966  lcdfval  32071  lcdval  32072  lcdvsub  32100  lcdvsubval  32101  mapdffval  32109  mapdfval  32110  hdmap1fval  32280  hdmapfval  32313  hgmapfval  32372  hdmapglem7  32415  hlhilset  32420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421
  Copyright terms: Public domain W3C validator