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

Theorem fveq12d 5862
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 5858 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5860 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2484 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586
This theorem is referenced by:  nffvd  5865  fvsng  6090  tfrlem3a  7048  resixpfo  7509  cantnfval  8090  cantnfres  8099  cantnfvalOLD  8120  fseqenlem1  8408  fseqenlem2  8409  dfac12lem1  8526  dfac12lem2  8527  dfac12r  8529  hsmexlem2  8810  ttukeylem3  8894  ttukey2g  8899  seq1  12101  expval  12149  lsw  12566  ccatfval  12573  swrdval  12625  splfv2a  12713  revval  12715  seqshft  12899  climshft2  13386  fprodser  13737  imasval  14889  funcid  15217  funcco  15218  funcoppc  15222  funcres  15243  nati  15302  evlf2  15465  evlf1  15467  evlfcl  15469  uncf2  15484  hofcl  15506  yonedalem21  15520  yonedalem3a  15521  yonedalem4a  15522  yonedalem4b  15523  yonedalem22  15525  yonedalem3  15527  yonedainv  15528  p0val  15649  p1val  15650  gsumvalx  15875  gsumpropd  15877  gsumval2a  15884  gsumccat  15987  mulgfval  16121  mulgval  16122  mulgnndir  16142  mulgpropd  16153  prdsinvlem  16156  cntrval  16335  efgsf  16725  efgsval  16727  issrngd  17488  rlmval  17815  evlseu  18163  evlval  18171  evls1fval  18334  evl1varpw  18375  chrval  18539  znval  18549  isphl  18640  isphld  18666  phlpropd  18667  cssval  18690  prdsinvgd2  18750  islindf  18824  madetsumid  18940  madufval  19116  smadiadetr  19154  decpmatval0  19242  chpmatfval  19308  isperf  19629  dfac14  20096  xkohmeo  20293  flffval  20467  fcfval  20511  cnextfval  20539  tsmsval2  20605  tsmspropd  20607  tngngp  21145  isnlm  21161  sranlm  21170  ovoliunlem1  21890  ovoliunlem2  21891  limcfval  22253  dvfval  22278  dvreslem  22290  dvaddbr  22318  dvmulbr  22319  isuc1p  22518  ismon1p  22520  q1pval  22531  dgreq0  22638  vieta1lem2  22683  vieta1  22684  basellem5  23334  lgsval  23551  lgsneg  23570  israg  24050  iswlkon  24510  iscrct  24600  iscycl  24601  isclwlk0  24730  gxfval  25235  dipfval  25588  rrhval  27954  xrhval  27973  brae  28190  braew  28191  sitmval  28267  sseqval  28304  fibp1  28317  elprob  28325  signsvtn0  28504  signstfvneq0  28506  signstfveq0  28511  cvmliftlem5  28711  cvmliftlem7  28713  cvmliftlem10  28716  cvmliftlem13  28718  mclsval  28900  rdgprc0  29201  dfrdg2  29203  wrecseq123  29312  sdclem2  30210  ismrc  30608  rmxfval  30815  rmyfval  30816  aomclem8  30982  hbt  31054  elmnc  31061  mncn0  31064  aaitgo  31087  mon1pid  31141  limciccioolb  31535  limcicciooub  31551  ioccncflimc  31595  icocncflimc  31599  dirkercncflem3  31776  fourierdlem32  31810  afveq12d  32056  funcestrcsetclem7  32501  funcestrcsetclem9  32503  funcringcsetcOLD2lem7  32587  funcringcsetcOLD2lem9  32589  funcringcsetclem7OLD  32610  funcringcsetclem9OLD  32612  bj-finsumval0  34403  ldualvsub  34620  ldualvsubval  34622  isopos  34645  polfvalN  35368  psubclsetN  35400  docaffvalN  36588  docafvalN  36589  djaffvalN  36600  djafvalN  36601  dihffval  36697  dihfval  36698  dochffval  36816  dochfval  36817  djhffval  36863  djhfval  36864  islpolN  36950  lcdfval  37055  lcdval  37056  lcdvsub  37084  lcdvsubval  37085  mapdffval  37093  mapdfval  37094  hdmap1fval  37264  hdmapfval  37297  hgmapfval  37356  hdmapglem7  37399  hlhilset  37404
  Copyright terms: Public domain W3C validator