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

Theorem fveq12d 6159
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 6155 . 2 (𝜑 → (𝐹𝐴) = (𝐺𝐴))
3 fveq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43fveq2d 6157 . 2 (𝜑 → (𝐺𝐴) = (𝐺𝐵))
52, 4eqtrd 2655 1 (𝜑 → (𝐹𝐴) = (𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cfv 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860
This theorem is referenced by:  nffvd  6162  fvsng  6407  wrecseq123  7360  tfrlem3a  7425  resixpfo  7897  cantnfval  8516  cantnfres  8525  fseqenlem1  8798  fseqenlem2  8799  dfac12lem1  8916  dfac12lem2  8917  dfac12r  8919  hsmexlem2  9200  ttukeylem3  9284  ttukey2g  9289  seq1  12761  expval  12809  lsw  13297  ccatfval  13304  swrdval  13362  splfv2a  13451  revval  13453  relexpsucnnr  13706  relexp1g  13707  seqshft  13766  climshft2  14254  fprodser  14611  imasval  16099  funcid  16458  funcco  16459  funcoppc  16463  funcres  16484  nati  16543  funcestrcsetclem7  16714  funcestrcsetclem9  16716  funcsetcestrclem7  16729  funcsetcestrclem9  16731  evlf2  16786  evlf1  16788  evlfcl  16790  uncf2  16805  hofcl  16827  yonedalem21  16841  yonedalem3a  16842  yonedalem4a  16843  yonedalem4b  16844  yonedalem22  16846  yonedalem3  16848  yonedainv  16849  p0val  16969  p1val  16970  gsumvalx  17198  gsumpropd  17200  gsumval2a  17207  gsumccat  17306  prdsinvlem  17452  mulgfval  17470  mulgval  17471  mulgnndir  17497  mulgnndirOLD  17498  mulgpropd  17512  cntrval  17680  efgsf  18070  efgsval  18072  issrngd  18789  rlmval  19119  evlseu  19444  evlval  19452  evls1fval  19612  evl1varpw  19653  chrval  19801  znval  19811  isphl  19901  isphld  19927  phlpropd  19928  cssval  19954  prdsinvgd2  20014  islindf  20079  madetsumid  20195  madufval  20371  smadiadetr  20409  decpmatval0  20497  chpmatfval  20563  isperf  20874  dfac14  21340  xkohmeo  21537  flffval  21712  fcfval  21756  cnextfval  21785  tsmsval2  21852  tsmspropd  21854  tngngp  22377  tngngp3  22379  isnlm  22398  sranlm  22407  cnncvsabsnegdemo  22884  ovoliunlem1  23189  ovoliunlem2  23190  limcfval  23555  dvfval  23580  dvreslem  23592  dvaddbr  23620  dvmulbr  23621  isuc1p  23817  ismon1p  23819  q1pval  23830  dgreq0  23938  vieta1lem2  23983  vieta1  23984  basellem5  24724  lgsval  24939  lgsneg  24959  israg  25505  iscgra  25614  iswlkon  26435  wlkres  26449  wlkp1lem3  26454  wlkp1lem6  26457  isclwlk  26551  iscrct  26567  iscycl  26568  eupth2eucrct  26956  dipfval  27424  lmatfval  29680  lmat22e11  29684  rrhval  29840  xrhval  29862  brae  30103  braew  30104  sitmval  30210  sseqval  30249  fibp1  30262  elprob  30270  signsvtn0  30445  signstfvneq0  30447  signstfveq0  30452  cvmliftlem5  31006  cvmliftlem7  31008  cvmliftlem10  31011  cvmliftlem13  31013  mclsval  31195  rdgprc0  31427  dfrdg2  31429  bj-finsumval0  32807  rdgeqoa  32877  finxpeq2  32883  finxpreclem6  32892  finxpsuclem  32893  sdclem2  33197  ldualvsub  33949  ldualvsubval  33951  isopos  33974  polfvalN  34697  psubclsetN  34729  docaffvalN  35917  docafvalN  35918  djaffvalN  35929  djafvalN  35930  dihffval  36026  dihfval  36027  dochffval  36145  dochfval  36146  djhffval  36192  djhfval  36193  islpolN  36279  lcdfval  36384  lcdval  36385  lcdvsub  36413  lcdvsubval  36414  mapdffval  36422  mapdfval  36423  hdmap1fval  36593  hdmapfval  36626  hgmapfval  36685  hdmapglem7  36728  hlhilset  36733  ismrc  36771  rmxfval  36975  rmyfval  36976  aomclem8  37138  hbt  37208  elmnc  37214  mncn0  37217  aaitgo  37240  mon1pid  37291  clsk1independent  37853  binomcxp  38065  limciccioolb  39280  limcicciooub  39296  ioccncflimc  39424  icocncflimc  39428  dvnprodlem2  39490  dvnprodlem3  39491  dirkercncflem3  39650  fourierdlem32  39684  etransclem32  39811  etransclem44  39823  etransclem46  39825  etransc  39828  ovnsubaddlem1  40112  ovnsubaddlem2  40113  ovnsubadd  40114  hoidmvlelem4  40140  hoidmvlelem5  40141  hspmbl  40171  vonioo  40224  vonicc  40227  afveq12d  40538  iccelpart  40688  nnsum3primesprm  40988  funcringcsetcALTV2lem7  41351  funcringcsetcALTV2lem9  41353  funcringcsetclem7ALTV  41374  funcringcsetclem9ALTV  41376
  Copyright terms: Public domain W3C validator