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

Theorem fveq12d 6310
Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
fveq12d.1 (𝜑𝐹 = 𝐺)
fveq12d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
fveq12d (𝜑 → (𝐹𝐴) = (𝐺𝐵))

Proof of Theorem fveq12d
StepHypRef Expression
1 fveq12d.1 . . 3 (𝜑𝐹 = 𝐺)
21fveq1d 6306 . 2 (𝜑 → (𝐹𝐴) = (𝐺𝐴))
3 fveq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43fveq2d 6308 . 2 (𝜑 → (𝐺𝐴) = (𝐺𝐵))
52, 4eqtrd 2758 1 (𝜑 → (𝐹𝐴) = (𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  cfv 6001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009
This theorem is referenced by:  nffvd  6313  fvsng  6563  wrecseq123  7528  tfrlem3a  7593  resixpfo  8063  cantnfval  8678  cantnfres  8687  fseqenlem1  8960  fseqenlem2  8961  dfac12lem1  9078  dfac12lem2  9079  dfac12r  9081  hsmexlem2  9362  ttukeylem3  9446  ttukey2g  9451  seq1  12929  expval  12977  lsw  13459  ccatfval  13466  swrdval  13537  splfv2a  13628  revval  13630  relexpsucnnr  13885  relexp1g  13886  seqshft  13945  climshft2  14433  fprodser  14799  imasval  16294  funcid  16652  funcco  16653  funcoppc  16657  funcres  16678  nati  16737  funcestrcsetclem7  16908  funcestrcsetclem9  16910  funcsetcestrclem7  16923  funcsetcestrclem9  16925  evlf2  16980  evlf1  16982  evlfcl  16984  uncf2  16999  hofcl  17021  yonedalem21  17035  yonedalem3a  17036  yonedalem4a  17037  yonedalem4b  17038  yonedalem22  17040  yonedalem3  17042  yonedainv  17043  p0val  17163  p1val  17164  gsumvalx  17392  gsumpropd  17394  gsumval2a  17401  gsumccat  17500  prdsinvlem  17646  mulgfval  17664  mulgval  17665  mulgnndir  17691  mulgnndirOLD  17692  mulgpropd  17706  cntrval  17873  efgsf  18263  efgsval  18265  issrngd  18984  rlmval  19314  evlseu  19639  evlval  19647  evls1fval  19807  evl1varpw  19848  chrval  19996  znval  20006  isphl  20096  isphld  20122  phlpropd  20123  cssval  20149  prdsinvgd2  20209  islindf  20274  madetsumid  20390  madufval  20566  smadiadetr  20604  decpmatval0  20692  chpmatfval  20758  isperf  21078  dfac14  21544  xkohmeo  21741  flffval  21915  fcfval  21959  cnextfval  21988  tsmsval2  22055  tsmspropd  22057  tngngp  22580  tngngp3  22582  isnlm  22601  sranlm  22610  cnncvsabsnegdemo  23086  ovoliunlem1  23391  ovoliunlem2  23392  limcfval  23756  dvfval  23781  dvreslem  23793  dvaddbr  23821  dvmulbr  23822  isuc1p  24020  ismon1p  24022  q1pval  24033  dgreq0  24141  vieta1lem2  24186  vieta1  24187  basellem5  24931  lgsval  25146  lgsneg  25166  israg  25712  iscgra  25821  iswlkon  26684  wlkres  26698  wlkp1lem3  26703  wlkp1lem6  26706  isclwlk  26800  iscrct  26817  iscycl  26818  eupth2eucrct  27290  dipfval  27787  lmatfval  30110  lmat22e11  30114  rrhval  30270  xrhval  30292  prodindf  30315  brae  30534  braew  30535  sitmval  30641  sseqval  30680  fibp1  30693  elprob  30701  signsvtn0  30877  signstfvneq0  30879  signstfveq0  30884  breprexplema  30938  breprexp  30941  circlevma  30950  circlemethhgt  30951  cvmliftlem5  31499  cvmliftlem7  31501  cvmliftlem10  31504  cvmliftlem13  31506  mclsval  31688  rdgprc0  31925  dfrdg2  31927  bj-finsumval0  33379  rdgeqoa  33450  finxpeq2  33456  finxpreclem6  33465  finxpsuclem  33466  sdclem2  33770  ldualvsub  34862  ldualvsubval  34864  isopos  34887  polfvalN  35610  psubclsetN  35642  docaffvalN  36829  docafvalN  36830  djaffvalN  36841  djafvalN  36842  dihffval  36938  dihfval  36939  dochffval  37057  dochfval  37058  djhffval  37104  djhfval  37105  islpolN  37191  lcdfval  37296  lcdval  37297  lcdvsub  37325  lcdvsubval  37326  mapdffval  37334  mapdfval  37335  hdmap1fval  37505  hdmapfval  37538  hgmapfval  37597  hdmapglem7  37640  hlhilset  37645  ismrc  37683  rmxfval  37887  rmyfval  37888  aomclem8  38050  hbt  38119  elmnc  38125  mncn0  38128  aaitgo  38151  mon1pid  38202  clsk1independent  38763  binomcxp  38975  limciccioolb  40273  limcicciooub  40289  ioccncflimc  40518  icocncflimc  40522  dvnprodlem2  40582  dvnprodlem3  40583  dirkercncflem3  40742  fourierdlem32  40776  etransclem32  40903  etransclem44  40915  etransclem46  40917  etransc  40920  ovnsubaddlem1  41207  ovnsubaddlem2  41208  ovnsubadd  41209  hoidmvlelem4  41235  hoidmvlelem5  41236  hspmbl  41266  vonioo  41319  vonicc  41322  afveq12d  41636  iccelpart  41796  nnsum3primesprm  42105  funcringcsetcALTV2lem7  42469  funcringcsetcALTV2lem9  42471  funcringcsetclem7ALTV  42492  funcringcsetclem9ALTV  42494
  Copyright terms: Public domain W3C validator