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

Theorem fveq12d 5893
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 5889 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5891 . 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 1454   ` cfv 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-iota 5564  df-fv 5608
This theorem is referenced by:  nffvd  5896  fvsng  6121  wrecseq123  7054  tfrlem3a  7120  resixpfo  7585  cantnfval  8198  cantnfres  8207  fseqenlem1  8480  fseqenlem2  8481  dfac12lem1  8598  dfac12lem2  8599  dfac12r  8601  hsmexlem2  8882  ttukeylem3  8966  ttukey2g  8971  seq1  12257  expval  12305  lsw  12746  ccatfval  12754  swrdval  12809  splfv2a  12899  revval  12901  relexpsucnnr  13136  relexp1g  13137  seqshft  13196  climshft2  13694  fprodser  14051  imasval  15459  imasvalOLD  15460  funcid  15823  funcco  15824  funcoppc  15828  funcres  15849  nati  15908  funcestrcsetclem7  16079  funcestrcsetclem9  16081  funcsetcestrclem7  16094  funcsetcestrclem9  16096  evlf2  16151  evlf1  16153  evlfcl  16155  uncf2  16170  hofcl  16192  yonedalem21  16206  yonedalem3a  16207  yonedalem4a  16208  yonedalem4b  16209  yonedalem22  16211  yonedalem3  16213  yonedainv  16214  p0val  16335  p1val  16336  gsumvalx  16561  gsumpropd  16563  gsumval2a  16570  gsumccat  16673  mulgfval  16807  mulgval  16808  mulgnndir  16828  mulgpropd  16839  prdsinvlem  16842  cntrval  17021  efgsf  17427  efgsval  17429  issrngd  18137  rlmval  18462  evlseu  18787  evlval  18795  evls1fval  18956  evl1varpw  18997  chrval  19144  znval  19154  isphl  19243  isphld  19269  phlpropd  19270  cssval  19293  prdsinvgd2  19353  islindf  19418  madetsumid  19534  madufval  19710  smadiadetr  19748  decpmatval0  19836  chpmatfval  19902  isperf  20215  dfac14  20681  xkohmeo  20878  flffval  21052  fcfval  21096  cnextfval  21125  tsmsval2  21192  tsmspropd  21194  tngngp  21710  isnlm  21726  sranlm  21735  ovoliunlem1  22503  ovoliunlem2  22504  limcfval  22875  dvfval  22900  dvreslem  22912  dvaddbr  22940  dvmulbr  22941  isuc1p  23139  ismon1p  23141  q1pval  23152  dgreq0  23267  vieta1lem2  23312  vieta1  23313  basellem5  24059  lgsval  24276  lgsneg  24295  israg  24790  iscgra  24899  iswlkon  25310  iscrct  25400  iscycl  25401  isclwlk0  25530  gxfval  26033  dipfval  26386  lmatfval  28688  lmat22e11  28692  rrhval  28848  xrhval  28870  brae  29112  braew  29113  sitmval  29230  sseqval  29269  fibp1  29282  elprob  29290  signsvtn0  29507  signstfvneq0  29509  signstfveq0  29514  cvmliftlem5  30060  cvmliftlem7  30062  cvmliftlem10  30065  cvmliftlem13  30067  mclsval  30249  rdgprc0  30488  dfrdg2  30490  bj-finsumval0  31746  rdgeqoa  31817  finxpeq2  31823  finxpreclem6  31832  finxpsuclem  31833  sdclem2  32115  ldualvsub  32765  ldualvsubval  32767  isopos  32790  polfvalN  33513  psubclsetN  33545  docaffvalN  34733  docafvalN  34734  djaffvalN  34745  djafvalN  34746  dihffval  34842  dihfval  34843  dochffval  34961  dochfval  34962  djhffval  35008  djhfval  35009  islpolN  35095  lcdfval  35200  lcdval  35201  lcdvsub  35229  lcdvsubval  35230  mapdffval  35238  mapdfval  35239  hdmap1fval  35409  hdmapfval  35442  hgmapfval  35501  hdmapglem7  35544  hlhilset  35549  ismrc  35587  rmxfval  35796  rmyfval  35797  aomclem8  35963  hbt  36033  elmnc  36039  mncn0  36042  aaitgo  36072  mon1pid  36126  binomcxp  36749  limciccioolb  37738  limcicciooub  37754  ioccncflimc  37800  icocncflimc  37804  dvnprodlem2  37859  dvnprodlem3  37860  dirkercncflem3  38004  fourierdlem32  38039  etransclem32  38168  etransclem44  38180  etransclem46  38182  etransc  38186  ovnsubaddlem1  38429  ovnsubaddlem2  38430  ovnsubadd  38431  hoidmvlelem4  38457  hoidmvlelem5  38458  hspmbl  38488  afveq12d  38672  iccelpart  38784  nnsum3primesprm  38922  iswlkOn  39707  isclWlk  39798  isCrct  39812  isCycl  39813  funcringcsetcALTV2lem7  40316  funcringcsetcALTV2lem9  40318  funcringcsetclem7ALTV  40339  funcringcsetclem9ALTV  40341
  Copyright terms: Public domain W3C validator