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

Theorem fveq12d 5857
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 5853 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5855 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2445 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407   ` cfv 5571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-iota 5535  df-fv 5579
This theorem is referenced by:  nffvd  5860  fvsng  6087  wrecseq123  7016  tfrlem3a  7082  resixpfo  7547  cantnfval  8121  cantnfres  8130  cantnfvalOLD  8151  fseqenlem1  8439  fseqenlem2  8440  dfac12lem1  8557  dfac12lem2  8558  dfac12r  8560  hsmexlem2  8841  ttukeylem3  8925  ttukey2g  8930  seq1  12166  expval  12214  lsw  12640  ccatfval  12648  swrdval  12700  splfv2a  12790  revval  12792  relexpsucnnr  13009  relexp1g  13010  seqshft  13069  climshft2  13556  fprodser  13910  imasval  15127  funcid  15485  funcco  15486  funcoppc  15490  funcres  15511  nati  15570  funcestrcsetclem7  15741  funcestrcsetclem9  15743  funcsetcestrclem7  15756  funcsetcestrclem9  15758  evlf2  15813  evlf1  15815  evlfcl  15817  uncf2  15832  hofcl  15854  yonedalem21  15868  yonedalem3a  15869  yonedalem4a  15870  yonedalem4b  15871  yonedalem22  15873  yonedalem3  15875  yonedainv  15876  p0val  15997  p1val  15998  gsumvalx  16223  gsumpropd  16225  gsumval2a  16232  gsumccat  16335  mulgfval  16469  mulgval  16470  mulgnndir  16490  mulgpropd  16501  prdsinvlem  16504  cntrval  16683  efgsf  17073  efgsval  17075  issrngd  17832  rlmval  18159  evlseu  18507  evlval  18515  evls1fval  18678  evl1varpw  18719  chrval  18864  znval  18874  isphl  18963  isphld  18989  phlpropd  18990  cssval  19013  prdsinvgd2  19073  islindf  19141  madetsumid  19257  madufval  19433  smadiadetr  19471  decpmatval0  19559  chpmatfval  19625  isperf  19947  dfac14  20413  xkohmeo  20610  flffval  20784  fcfval  20828  cnextfval  20856  tsmsval2  20922  tsmspropd  20924  tngngp  21462  isnlm  21478  sranlm  21487  ovoliunlem1  22207  ovoliunlem2  22208  limcfval  22570  dvfval  22595  dvreslem  22607  dvaddbr  22635  dvmulbr  22636  isuc1p  22835  ismon1p  22837  q1pval  22848  dgreq0  22956  vieta1lem2  23001  vieta1  23002  basellem5  23741  lgsval  23958  lgsneg  23977  israg  24464  iswlkon  24963  iscrct  25053  iscycl  25054  isclwlk0  25183  gxfval  25686  dipfval  26039  rrhval  28442  xrhval  28461  brae  28703  braew  28704  sitmval  28809  sseqval  28846  fibp1  28859  elprob  28867  signsvtn0  29046  signstfvneq0  29048  signstfveq0  29053  cvmliftlem5  29599  cvmliftlem7  29601  cvmliftlem10  29604  cvmliftlem13  29606  mclsval  29788  rdgprc0  30026  dfrdg2  30028  bj-finsumval0  31240  sdclem2  31530  ldualvsub  32186  ldualvsubval  32188  isopos  32211  polfvalN  32934  psubclsetN  32966  docaffvalN  34154  docafvalN  34155  djaffvalN  34166  djafvalN  34167  dihffval  34263  dihfval  34264  dochffval  34382  dochfval  34383  djhffval  34429  djhfval  34430  islpolN  34516  lcdfval  34621  lcdval  34622  lcdvsub  34650  lcdvsubval  34651  mapdffval  34659  mapdfval  34660  hdmap1fval  34830  hdmapfval  34863  hgmapfval  34922  hdmapglem7  34965  hlhilset  34970  ismrc  35008  rmxfval  35214  rmyfval  35215  aomclem8  35382  hbt  35456  elmnc  35462  mncn0  35465  aaitgo  35488  mon1pid  35542  binomcxp  36123  limciccioolb  37008  limcicciooub  37024  ioccncflimc  37069  icocncflimc  37073  dvnprodlem2  37125  dvnprodlem3  37126  dirkercncflem3  37268  fourierdlem32  37302  etransclem32  37430  etransclem44  37442  etransclem46  37444  etransc  37447  afveq12d  37599  iccelpart  37713  nnsum3primesprm  37851  funcringcsetcALTV2lem7  38374  funcringcsetcALTV2lem9  38376  funcringcsetclem7ALTV  38397  funcringcsetclem9ALTV  38399
  Copyright terms: Public domain W3C validator