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

Theorem fveq12d 5726
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 5722 . 2  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
3 fveq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43fveq2d 5724 . 2  |-  ( ph  ->  ( G `  A
)  =  ( G `
 B ) )
52, 4eqtrd 2467 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   ` cfv 5446
This theorem is referenced by:  nffvd  5729  fvsng  5919  resixpfo  7092  cantnfval  7615  cantnfres  7625  fseqenlem1  7897  fseqenlem2  7898  dfac12lem1  8015  dfac12lem2  8016  dfac12r  8018  hsmexlem2  8299  ttukeylem3  8383  ttukey2g  8388  seq1  11328  expval  11376  ccatfval  11734  swrdval  11756  splfv2a  11777  revval  11784  seqshft  11892  climshft2  12368  imasval  13729  funcid  14059  funcco  14060  funcoppc  14064  funcres  14085  nati  14144  evlf2  14307  evlf1  14309  evlfcl  14311  uncf2  14326  hofcl  14348  yonedalem21  14362  yonedalem3a  14363  yonedalem4a  14364  yonedalem4b  14365  yonedalem22  14367  yonedalem3  14369  yonedainv  14370  p0val  14462  p1val  14463  gsumvalx  14766  gsumpropd  14768  gsumval2a  14774  gsumccat  14779  mulgfval  14883  mulgval  14884  mulgnndir  14904  mulgpropd  14915  prdsinvlem  14918  cntrval  15110  efgsf  15353  efgsval  15355  issrngd  15941  rlmval  16256  chrval  16798  znval  16808  isphl  16851  isphld  16877  phlpropd  16878  cssval  16901  isperf  17207  dfac14  17642  xkohmeo  17839  flffval  18013  fcfval  18057  cnextfval  18085  tsmsval2  18151  tsmspropd  18153  tngngp  18687  isnlm  18703  sranlm  18712  ovoliunlem1  19390  ovoliunlem2  19391  limcfval  19751  dvfval  19776  dvreslem  19788  dvaddbr  19816  dvmulbr  19817  evlseu  19929  evlval  19937  isuc1p  20055  ismon1p  20057  q1pval  20068  dgreq0  20175  vieta1lem2  20220  vieta1  20221  basellem5  20859  lgsval  21076  lgsneg  21095  iswlkon  21523  iscrct  21603  iscycl  21604  gxfval  21837  dipfval  22190  rrhval  24371  xrhval  24376  brae  24584  braew  24585  sitmval  24653  elprob  24659  cvmliftlem5  24968  cvmliftlem7  24970  cvmliftlem10  24973  cvmliftlem13  24975  fprodser  25267  rdgprc0  25413  dfrdg2  25415  wrecseq123  25524  sdclem2  26437  ismrc  26746  rmxfval  26958  rmyfval  26959  aomclem8  27127  prdsinvgd2  27176  islindf  27250  hbt  27302  elmnc  27309  mncn0  27312  aaitgo  27335  mdetfval  27455  mon1pid  27492  afveq12d  27964  lswrd  28225  ldualvsub  29890  ldualvsubval  29892  isopos  29915  polfvalN  30638  psubclsetN  30670  docaffvalN  31856  docafvalN  31857  djaffvalN  31868  djafvalN  31869  dihffval  31965  dihfval  31966  dochffval  32084  dochfval  32085  djhffval  32131  djhfval  32132  islpolN  32218  lcdfval  32323  lcdval  32324  lcdvsub  32352  lcdvsubval  32353  mapdffval  32361  mapdfval  32362  hdmap1fval  32532  hdmapfval  32565  hgmapfval  32624  hdmapglem7  32667  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454
  Copyright terms: Public domain W3C validator