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

Theorem fveq12d 5674
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 5670 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5672 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2419 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ` cfv 5394
This theorem is referenced by:  nffvd  5677  fvsng  5866  resixpfo  7036  cantnfval  7556  cantnfres  7566  fseqenlem1  7838  fseqenlem2  7839  dfac12lem1  7956  dfac12lem2  7957  dfac12r  7959  hsmexlem2  8240  ttukeylem3  8324  ttukey2g  8329  seq1  11263  expval  11311  ccatfval  11669  swrdval  11691  splfv2a  11712  revval  11719  seqshft  11827  climshft2  12303  imasval  13664  funcid  13994  funcco  13995  funcoppc  13999  funcres  14020  nati  14079  evlf2  14242  evlf1  14244  evlfcl  14246  uncf2  14261  hofcl  14283  yonedalem21  14297  yonedalem3a  14298  yonedalem4a  14299  yonedalem4b  14300  yonedalem22  14302  yonedalem3  14304  yonedainv  14305  p0val  14397  p1val  14398  gsumvalx  14701  gsumpropd  14703  gsumval2a  14709  gsumccat  14714  mulgfval  14818  mulgval  14819  mulgnndir  14839  mulgpropd  14850  prdsinvlem  14853  cntrval  15045  efgsf  15288  efgsval  15290  issrngd  15876  rlmval  16191  chrval  16729  znval  16739  isphl  16782  isphld  16808  phlpropd  16809  cssval  16832  isperf  17137  dfac14  17571  xkohmeo  17768  flffval  17942  fcfval  17986  cnextfval  18014  tsmsval2  18080  tsmspropd  18082  tngngp  18566  isnlm  18582  sranlm  18591  ovoliunlem1  19265  ovoliunlem2  19266  limcfval  19626  dvfval  19651  dvreslem  19663  dvaddbr  19691  dvmulbr  19692  evlseu  19804  evlval  19812  isuc1p  19930  ismon1p  19932  q1pval  19943  dgreq0  20050  vieta1lem2  20095  vieta1  20096  basellem5  20734  lgsval  20951  lgsneg  20970  iswlkon  21395  iscrct  21459  iscycl  21460  gxfval  21693  dipfval  22046  rrhval  24178  brae  24386  braew  24387  elprob  24446  cvmliftlem5  24755  cvmliftlem7  24757  cvmliftlem10  24760  cvmliftlem13  24762  fprodser  25054  rdgprc0  25174  dfrdg2  25176  sdclem2  26137  ismrc  26446  rmxfval  26658  rmyfval  26659  aomclem8  26828  prdsinvgd2  26877  islindf  26951  hbt  27003  elmnc  27010  mncn0  27013  aaitgo  27036  mdetfval  27156  mon1pid  27193  afveq12d  27666  ldualvsub  29270  ldualvsubval  29272  isopos  29295  polfvalN  30018  psubclsetN  30050  docaffvalN  31236  docafvalN  31237  djaffvalN  31248  djafvalN  31249  dihffval  31345  dihfval  31346  dochffval  31464  dochfval  31465  djhffval  31511  djhfval  31512  islpolN  31598  lcdfval  31703  lcdval  31704  lcdvsub  31732  lcdvsubval  31733  mapdffval  31741  mapdfval  31742  hdmap1fval  31912  hdmapfval  31945  hgmapfval  32004  hdmapglem7  32047  hlhilset  32052
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402
  Copyright terms: Public domain W3C validator