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

Theorem reseq1d 5277
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqd.1
Assertion
Ref Expression
reseq1d

Proof of Theorem reseq1d
StepHypRef Expression
1 reseqd.1 . 2
2 reseq1 5272 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  |`cres 5006
This theorem is referenced by:  reseq12d  5279  fun2ssres  5634  funcnvres2  5664  fresin  5759  fresaunres2  5762  offres  6795  itunifval  8817  hsmex  8833  gruima  9201  fseq1p1m1  11781  ltweuz  12072  rlimres  13381  lo1res  13382  lo1resb  13387  rlimresb  13388  o1resb  13389  bitsf1ocnv  14094  fsets  14658  setsres  14660  setscom  14662  sscres  15192  resfval2  15262  psgnunilem5  16519  gsumzres  16914  gsumzresOLD  16918  gsumzsplit  16944  gsumzsplitOLD  16945  gsum2dlem2  16998  gsum2dOLD  17000  dpjidcl  17107  dpjidclOLD  17114  pgpfaclem1  17132  pwssplit2  17706  pwssplit3  17707  znle2  18592  mamures  18892  ofco2  18953  mdetunilem9  19122  mdetmul  19125  smadiadetglem1  19173  smadiadetglem2  19174  tmdgsum  20594  tsmsval2  20628  tsmsresOLD  20645  tsmsres  20646  tsmssplit  20654  imasdsf1olem  20876  tmslem  20985  sranlm  21193  srabn  21800  mbflimsup  22073  dvres  22315  dvres3a  22318  dvnres  22334  cpnres  22340  dvcmul  22347  dvcmulf  22348  dvcobr  22349  dvmptres3  22359  dvmptres2  22365  dvcnvlem  22377  dvlip2  22396  ftc2ditglem  22446  aannenlem1  22724  eff1olem  22935  resqrtcn  23123  sqrtcn  23124  rlimcnp2  23296  jensenlem2  23317  ex-res  25162  drngoi  25409  rabfodom  27404  resf1o  27553  zhmnrg  27948  indf1ofs  28039  fibp1  28340  cvmliftlem10  28739  cvmlift2lem6  28753  cvmlift2lem12  28759  trpredeq1  29303  trpredeq2  29304  trpredeq3  29305  ftc1anclem8  30097  ftc2nc  30099  cocnv  30216  cnpwstotbnd  30293  eldioph2  30695  itgpowd  31182  dvsconst  31235  cncfmptss  31581  dvmptresicc  31716  itgsinexplem1  31752  itgcoscmulx  31768  itgiccshift  31779  itgperiod  31780  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem28  31917  fourierdlem42  31931  fourierdlem78  31967  fourierdlem81  31970  fourierdlem83  31972  fourierdlem84  31973  fourierdlem90  31979  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  estrres  32645  funcrngcsetc  32806  funcringcsetc  32843  rhmsubclem1  32894  rhmsubcOLDlem1  32913  aacllem  33216
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-an 371  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-v 3111  df-in 3482  df-res 5016
  Copyright terms: Public domain W3C validator