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

Theorem fveq12d 5885
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 5881 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5883 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2464 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438   ` cfv 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607
This theorem is referenced by:  nffvd  5888  fvsng  6111  wrecseq123  7035  tfrlem3a  7101  resixpfo  7566  cantnfval  8176  cantnfres  8185  fseqenlem1  8457  fseqenlem2  8458  dfac12lem1  8575  dfac12lem2  8576  dfac12r  8578  hsmexlem2  8859  ttukeylem3  8943  ttukey2g  8948  seq1  12227  expval  12275  lsw  12709  ccatfval  12717  swrdval  12769  splfv2a  12859  revval  12861  relexpsucnnr  13082  relexp1g  13083  seqshft  13142  climshft2  13639  fprodser  13996  imasval  15404  imasvalOLD  15405  funcid  15768  funcco  15769  funcoppc  15773  funcres  15794  nati  15853  funcestrcsetclem7  16024  funcestrcsetclem9  16026  funcsetcestrclem7  16039  funcsetcestrclem9  16041  evlf2  16096  evlf1  16098  evlfcl  16100  uncf2  16115  hofcl  16137  yonedalem21  16151  yonedalem3a  16152  yonedalem4a  16153  yonedalem4b  16154  yonedalem22  16156  yonedalem3  16158  yonedainv  16159  p0val  16280  p1val  16281  gsumvalx  16506  gsumpropd  16508  gsumval2a  16515  gsumccat  16618  mulgfval  16752  mulgval  16753  mulgnndir  16773  mulgpropd  16784  prdsinvlem  16787  cntrval  16966  efgsf  17372  efgsval  17374  issrngd  18082  rlmval  18407  evlseu  18732  evlval  18740  evls1fval  18901  evl1varpw  18942  chrval  19088  znval  19098  isphl  19187  isphld  19213  phlpropd  19214  cssval  19237  prdsinvgd2  19297  islindf  19362  madetsumid  19478  madufval  19654  smadiadetr  19692  decpmatval0  19780  chpmatfval  19846  isperf  20159  dfac14  20625  xkohmeo  20822  flffval  20996  fcfval  21040  cnextfval  21069  tsmsval2  21136  tsmspropd  21138  tngngp  21654  isnlm  21670  sranlm  21679  ovoliunlem1  22447  ovoliunlem2  22448  limcfval  22819  dvfval  22844  dvreslem  22856  dvaddbr  22884  dvmulbr  22885  isuc1p  23083  ismon1p  23085  q1pval  23096  dgreq0  23211  vieta1lem2  23256  vieta1  23257  basellem5  24003  lgsval  24220  lgsneg  24239  israg  24734  iscgra  24843  iswlkon  25254  iscrct  25344  iscycl  25345  isclwlk0  25474  gxfval  25977  dipfval  26330  lmatfval  28642  lmat22e11  28646  rrhval  28802  xrhval  28824  brae  29066  braew  29067  sitmval  29184  sseqval  29223  fibp1  29236  elprob  29244  signsvtn0  29461  signstfvneq0  29463  signstfveq0  29468  cvmliftlem5  30014  cvmliftlem7  30016  cvmliftlem10  30019  cvmliftlem13  30021  mclsval  30203  rdgprc0  30441  dfrdg2  30443  bj-finsumval0  31660  sdclem2  31991  ldualvsub  32646  ldualvsubval  32648  isopos  32671  polfvalN  33394  psubclsetN  33426  docaffvalN  34614  docafvalN  34615  djaffvalN  34626  djafvalN  34627  dihffval  34723  dihfval  34724  dochffval  34842  dochfval  34843  djhffval  34889  djhfval  34890  islpolN  34976  lcdfval  35081  lcdval  35082  lcdvsub  35110  lcdvsubval  35111  mapdffval  35119  mapdfval  35120  hdmap1fval  35290  hdmapfval  35323  hgmapfval  35382  hdmapglem7  35425  hlhilset  35430  ismrc  35468  rmxfval  35678  rmyfval  35679  aomclem8  35845  hbt  35915  elmnc  35921  mncn0  35924  aaitgo  35954  mon1pid  36008  binomcxp  36570  limciccioolb  37527  limcicciooub  37543  ioccncflimc  37589  icocncflimc  37593  dvnprodlem2  37648  dvnprodlem3  37649  dirkercncflem3  37793  fourierdlem32  37828  etransclem32  37957  etransclem44  37969  etransclem46  37971  etransc  37975  ovnsubaddlem1  38173  ovnsubaddlem2  38174  ovnsubadd  38175  afveq12d  38353  iccelpart  38465  nnsum3primesprm  38603  funcringcsetcALTV2lem7  39348  funcringcsetcALTV2lem9  39350  funcringcsetclem7ALTV  39371  funcringcsetclem9ALTV  39373
  Copyright terms: Public domain W3C validator