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

Theorem fveq12d 6338
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 6334 . 2 (𝜑 → (𝐹𝐴) = (𝐺𝐴))
3 fveq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43fveq2d 6336 . 2 (𝜑 → (𝐺𝐴) = (𝐺𝐵))
52, 4eqtrd 2805 1 (𝜑 → (𝐹𝐴) = (𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039
This theorem is referenced by:  nffvd  6341  fvsng  6591  wrecseq123  7560  tfrlem3a  7626  resixpfo  8100  cantnfval  8729  cantnfres  8738  fseqenlem1  9047  fseqenlem2  9048  dfac12lem1  9167  dfac12lem2  9168  dfac12r  9170  hsmexlem2  9451  ttukeylem3  9535  ttukey2g  9540  seq1  13021  expval  13069  lsw  13548  ccatfval  13555  swrdval  13625  splfv2a  13716  revval  13718  relexpsucnnr  13973  relexp1g  13974  seqshft  14033  climshft2  14521  fprodser  14886  imasval  16379  funcid  16737  funcco  16738  funcoppc  16742  funcres  16763  nati  16822  funcestrcsetclem7  16994  funcestrcsetclem9  16996  funcsetcestrclem7  17009  funcsetcestrclem9  17011  evlf2  17066  evlf1  17068  evlfcl  17070  uncf2  17085  hofcl  17107  yonedalem21  17121  yonedalem3a  17122  yonedalem4a  17123  yonedalem4b  17124  yonedalem22  17126  yonedalem3  17128  yonedainv  17129  p0val  17249  p1val  17250  gsumvalx  17478  gsumpropd  17480  gsumval2a  17487  gsumccat  17586  prdsinvlem  17732  mulgfval  17750  mulgval  17751  mulgnndir  17777  mulgnndirOLD  17778  mulgpropd  17792  cntrval  17959  efgsf  18349  efgsval  18351  issrngd  19071  rlmval  19406  evlseu  19731  evlval  19739  evls1fval  19899  evl1varpw  19940  chrval  20088  znval  20098  isphl  20190  isphld  20216  phlpropd  20217  cssval  20243  prdsinvgd2  20303  islindf  20368  madetsumid  20485  madufval  20661  smadiadetr  20700  decpmatval0  20789  chpmatfval  20855  isperf  21176  dfac14  21642  xkohmeo  21839  flffval  22013  fcfval  22057  cnextfval  22086  tsmsval2  22153  tsmspropd  22155  tngngp  22678  tngngp3  22680  isnlm  22699  sranlm  22708  cnncvsabsnegdemo  23184  ovoliunlem1  23490  ovoliunlem2  23491  limcfval  23856  dvfval  23881  dvreslem  23893  dvaddbr  23921  dvmulbr  23922  isuc1p  24120  ismon1p  24122  q1pval  24133  dgreq0  24241  vieta1lem2  24286  vieta1  24287  basellem5  25032  lgsval  25247  lgsneg  25267  israg  25813  iscgra  25922  iswlkon  26788  wlkres  26802  wlkp1lem3  26807  wlkp1lem6  26810  isclwlk  26904  iscrct  26921  iscycl  26922  eupth2eucrct  27397  dipfval  27897  lmatfval  30220  lmat22e11  30224  rrhval  30380  xrhval  30402  prodindf  30425  brae  30644  braew  30645  sitmval  30751  sseqval  30790  fibp1  30803  elprob  30811  signsvtn0  30987  signstfvneq0  30989  signstfveq0  30994  breprexplema  31048  breprexp  31051  circlevma  31060  circlemethhgt  31061  cvmliftlem5  31609  cvmliftlem7  31611  cvmliftlem10  31614  cvmliftlem13  31616  mclsval  31798  rdgprc0  32035  dfrdg2  32037  bj-finsumval0  33484  rdgeqoa  33555  finxpeq2  33561  finxpreclem6  33570  finxpsuclem  33571  sdclem2  33870  ldualvsub  34964  ldualvsubval  34966  isopos  34989  polfvalN  35712  psubclsetN  35744  docaffvalN  36931  docafvalN  36932  djaffvalN  36943  djafvalN  36944  dihffval  37040  dihfval  37041  dochffval  37159  dochfval  37160  djhffval  37206  djhfval  37207  islpolN  37293  lcdfval  37398  lcdval  37399  lcdvsub  37427  lcdvsubval  37428  mapdffval  37436  mapdfval  37437  hdmap1fval  37606  hdmapfval  37637  hgmapfval  37696  hdmapglem7  37739  hlhilset  37744  ismrc  37790  rmxfval  37994  rmyfval  37995  aomclem8  38157  hbt  38226  elmnc  38232  mncn0  38235  aaitgo  38258  mon1pid  38309  clsk1independent  38870  binomcxp  39082  limciccioolb  40371  limcicciooub  40387  ioccncflimc  40616  icocncflimc  40620  dvnprodlem2  40680  dvnprodlem3  40681  dirkercncflem3  40839  fourierdlem32  40873  etransclem32  41000  etransclem44  41012  etransclem46  41014  etransc  41017  ovnsubaddlem1  41304  ovnsubaddlem2  41305  ovnsubadd  41306  hoidmvlelem4  41332  hoidmvlelem5  41333  hspmbl  41363  vonioo  41416  vonicc  41419  afveq12d  41733  iccelpart  41897  nnsum3primesprm  42206  funcringcsetcALTV2lem7  42570  funcringcsetcALTV2lem9  42572  funcringcsetclem7ALTV  42593  funcringcsetclem9ALTV  42595
  Copyright terms: Public domain W3C validator