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

Theorem fveq12d 5692
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 5688 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5690 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2470 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421
This theorem is referenced by:  nffvd  5695  fvsng  5907  tfrlem3a  6828  resixpfo  7293  cantnfval  7868  cantnfres  7877  cantnfvalOLD  7898  fseqenlem1  8186  fseqenlem2  8187  dfac12lem1  8304  dfac12lem2  8305  dfac12r  8307  hsmexlem2  8588  ttukeylem3  8672  ttukey2g  8677  seq1  11811  expval  11859  lsw  12258  ccatfval  12265  swrdval  12305  splfv2a  12390  revval  12392  seqshft  12566  climshft2  13052  imasval  14441  funcid  14772  funcco  14773  funcoppc  14777  funcres  14798  nati  14857  evlf2  15020  evlf1  15022  evlfcl  15024  uncf2  15039  hofcl  15061  yonedalem21  15075  yonedalem3a  15076  yonedalem4a  15077  yonedalem4b  15078  yonedalem22  15080  yonedalem3  15082  yonedainv  15083  p0val  15203  p1val  15204  gsumvalx  15493  gsumpropd  15495  gsumval2a  15503  gsumccat  15510  mulgfval  15619  mulgval  15620  mulgnndir  15640  mulgpropd  15651  prdsinvlem  15654  cntrval  15828  efgsf  16217  efgsval  16219  issrngd  16926  rlmval  17252  evlseu  17582  evlval  17590  evls1fval  17734  evl1varpw  17775  chrval  17936  znval  17946  isphl  18037  isphld  18063  phlpropd  18064  cssval  18087  prdsinvgd2  18147  islindf  18221  madetsumid  18326  madufval  18423  smadiadetr  18461  isperf  18735  dfac14  19171  xkohmeo  19368  flffval  19542  fcfval  19586  cnextfval  19614  tsmsval2  19680  tsmspropd  19682  tngngp  20220  isnlm  20236  sranlm  20245  rrxmval  20884  ovoliunlem1  20965  ovoliunlem2  20966  limcfval  21327  dvfval  21352  dvreslem  21364  dvaddbr  21392  dvmulbr  21393  isuc1p  21592  ismon1p  21594  q1pval  21605  dgreq0  21712  vieta1lem2  21757  vieta1  21758  basellem5  22402  lgsval  22619  lgsneg  22638  israg  23068  iswlkon  23398  iscrct  23478  iscycl  23479  gxfval  23712  dipfval  24065  rrhval  26394  xrhval  26413  brae  26626  braew  26627  sitmval  26703  sseqval  26740  fibp1  26753  elprob  26761  signsvtn0  26940  signstfvneq0  26942  signstfveq0  26947  signsvvfval  26948  cvmliftlem5  27147  cvmliftlem7  27149  cvmliftlem10  27152  cvmliftlem13  27154  fprodser  27431  rdgprc0  27576  dfrdg2  27578  wrecseq123  27687  sdclem2  28609  ismrc  29008  rmxfval  29216  rmyfval  29217  aomclem8  29385  hbt  29457  elmnc  29464  mncn0  29467  aaitgo  29490  mon1pid  29544  afveq12d  30010  isclwlk0  30390  pmatcollpw1lem1  30856  bj-finsumval0  32479  ldualvsub  32693  ldualvsubval  32695  isopos  32718  polfvalN  33441  psubclsetN  33473  docaffvalN  34659  docafvalN  34660  djaffvalN  34671  djafvalN  34672  dihffval  34768  dihfval  34769  dochffval  34887  dochfval  34888  djhffval  34934  djhfval  34935  islpolN  35021  lcdfval  35126  lcdval  35127  lcdvsub  35155  lcdvsubval  35156  mapdffval  35164  mapdfval  35165  hdmap1fval  35335  hdmapfval  35368  hgmapfval  35427  hdmapglem7  35470  hlhilset  35475
  Copyright terms: Public domain W3C validator