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

Theorem fveq12d 5877
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 5873 . 2
3 fveq12d.2 . . 3
43fveq2d 5875 . 2
52, 4eqtrd 2498 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  `cfv 5593
This theorem is referenced by:  nffvd  5880  fvsng  6105  tfrlem3a  7065  resixpfo  7527  cantnfval  8108  cantnfres  8117  cantnfvalOLD  8138  fseqenlem1  8426  fseqenlem2  8427  dfac12lem1  8544  dfac12lem2  8545  dfac12r  8547  hsmexlem2  8828  ttukeylem3  8912  ttukey2g  8917  seq1  12120  expval  12168  lsw  12585  ccatfval  12592  swrdval  12644  splfv2a  12732  revval  12734  seqshft  12918  climshft2  13405  fprodser  13756  imasval  14908  funcid  15239  funcco  15240  funcoppc  15244  funcres  15265  nati  15324  evlf2  15487  evlf1  15489  evlfcl  15491  uncf2  15506  hofcl  15528  yonedalem21  15542  yonedalem3a  15543  yonedalem4a  15544  yonedalem4b  15545  yonedalem22  15547  yonedalem3  15549  yonedainv  15550  p0val  15671  p1val  15672  gsumvalx  15897  gsumpropd  15899  gsumval2a  15906  gsumccat  16009  mulgfval  16143  mulgval  16144  mulgnndir  16164  mulgpropd  16175  prdsinvlem  16178  cntrval  16357  efgsf  16747  efgsval  16749  issrngd  17510  rlmval  17837  evlseu  18185  evlval  18193  evls1fval  18356  evl1varpw  18397  chrval  18562  znval  18572  isphl  18663  isphld  18689  phlpropd  18690  cssval  18713  prdsinvgd2  18773  islindf  18847  madetsumid  18963  madufval  19139  smadiadetr  19177  decpmatval0  19265  chpmatfval  19331  isperf  19652  dfac14  20119  xkohmeo  20316  flffval  20490  fcfval  20534  cnextfval  20562  tsmsval2  20628  tsmspropd  20630  tngngp  21168  isnlm  21184  sranlm  21193  ovoliunlem1  21913  ovoliunlem2  21914  limcfval  22276  dvfval  22301  dvreslem  22313  dvaddbr  22341  dvmulbr  22342  isuc1p  22541  ismon1p  22543  q1pval  22554  dgreq0  22662  vieta1lem2  22707  vieta1  22708  basellem5  23358  lgsval  23575  lgsneg  23594  israg  24074  iswlkon  24534  iscrct  24624  iscycl  24625  isclwlk0  24754  gxfval  25259  dipfval  25612  rrhval  27977  xrhval  27996  brae  28213  braew  28214  sitmval  28290  sseqval  28327  fibp1  28340  elprob  28348  signsvtn0  28527  signstfvneq0  28529  signstfveq0  28534  cvmliftlem5  28734  cvmliftlem7  28736  cvmliftlem10  28739  cvmliftlem13  28741  mclsval  28923  rdgprc0  29226  dfrdg2  29228  wrecseq123  29337  sdclem2  30235  ismrc  30633  rmxfval  30840  rmyfval  30841  aomclem8  31007  hbt  31079  elmnc  31085  mncn0  31088  aaitgo  31111  mon1pid  31165  binomcxp  31262  limciccioolb  31627  limcicciooub  31643  ioccncflimc  31688  icocncflimc  31692  dvnprodlem2  31744  dvnprodlem3  31745  dirkercncflem3  31887  fourierdlem32  31921  etransclem32  32049  etransclem44  32061  etransclem46  32063  etransc  32066  afveq12d  32218  funcestrcsetclem7  32652  funcestrcsetclem9  32654  funcsetcestrclem7  32667  funcsetcestrclem9  32669  funcringcsetcOLD2lem7  32850  funcringcsetcOLD2lem9  32852  funcringcsetclem7OLD  32873  funcringcsetclem9OLD  32875  bj-finsumval0  34663  ldualvsub  34880  ldualvsubval  34882  isopos  34905  polfvalN  35628  psubclsetN  35660  docaffvalN  36848  docafvalN  36849  djaffvalN  36860  djafvalN  36861  dihffval  36957  dihfval  36958  dochffval  37076  dochfval  37077  djhffval  37123  djhfval  37124  islpolN  37210  lcdfval  37315  lcdval  37316  lcdvsub  37344  lcdvsubval  37345  mapdffval  37353  mapdfval  37354  hdmap1fval  37524  hdmapfval  37557  hgmapfval  37616  hdmapglem7  37659  hlhilset  37664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator