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

Theorem reseq2d 5278
Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqd.1
Assertion
Ref Expression
reseq2d

Proof of Theorem reseq2d
StepHypRef Expression
1 reseqd.1 . 2
2 reseq2 5273 . 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  resima2  5312  resdmdfsn  5324  relresfld  5539  f1orescnv  5836  funcocnv2  5845  fococnv2  5846  fvn0ssdmfun  6022  fnressn  6083  fnsnsplit  6108  oprssov  6444  curry1  6892  curry2  6895  dftpos2  6991  tfrlem16  7081  sbthlem4  7650  mapunen  7706  hartogslem1  7988  axdc3lem2  8852  fseq1p1m1  11781  hashf1lem1  12504  setsval  14656  idfuval  15245  idfu2nd  15246  resf1st  15263  setcid  15413  catcisolem  15433  1stfval  15460  1stf2  15462  2ndfval  15463  2ndf2  15465  1stfcl  15466  2ndfcl  15467  curf2ndf  15516  hofcl  15528  isps  15832  cnvps  15842  isdir  15862  dirref  15865  tsrdir  15868  frmdval  16019  frmdplusg  16022  gsum2dlem2  16998  gsum2dOLD  17000  dprd2da  17091  dpjval  17105  ablfac1eulem  17123  ablfac1eu  17124  psrplusg  18034  opsrtoslem2  18149  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  imacmp  19897  ptuncnv  20308  tgphaus  20615  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  tsmsxplem2  20656  trust  20732  metreslem  20865  imasdsf1olem  20876  xmspropd  20976  mspropd  20977  imasf1oxms  20992  imasf1oms  20993  nmpropd2  21115  isngp2  21117  ngppropd  21151  tngngp2  21166  cmspropd  21788  mbfres2  22052  limciun  22298  dvmptres3  22359  dvmptres2  22365  dvmptntr  22374  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  lhop1lem  22414  dvcnvrelem1  22418  dvcvx  22421  ftc2ditglem  22446  wilthlem2  23343  dchrval  23509  dchrelbas2  23512  ausisusgraedg  24356  1pthonlem1  24591  constr2pth  24603  eupath2lem3  24979  eupath2  24980  efghgrpOLD  25375  drngoi  25409  isdivrngo  25433  hhssablo  26179  hhssnvt  26181  hhsssh  26185  resf1o  27553  qtophaus  27839  esumcvg  28092  eulerpartlemn  28320  sseqp1  28334  signsvtn0  28527  cvmliftlem5  28734  cvmliftlem7  28736  cvmliftlem10  28739  cvmliftlem11  28740  cvmliftlem15  28743  cvmlift2lem11  28758  cvmlift2lem12  28759  ghomgrplem  29029  relexp0  29052  relexpsucr  29053  dfrtrcl2  29071  eldm3  29191  funsseq  29199  wrecseq123  29337  wfr3g  29342  wfrlem1  29343  wfrlem4  29346  wfrlem14  29356  wfr2  29360  tfrALTlem  29362  tfr2ALT  29364  tfr3ALT  29365  frr3g  29386  frrlem1  29387  frrlem4  29390  bpolylem  29810  finixpnum  30038  sdclem2  30235  prdsbnd2  30291  eldiophb  30690  diophrw  30692  diophin  30706  sblpnf  31190  fresin2  31448  cncfuni  31689  dvresntr  31713  dvbdfbdioolem1  31725  itgiccshift  31779  itgperiod  31780  dirkercncflem2  31886  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem58  31947  fourierdlem72  31961  fourierdlem74  31963  fourierdlem75  31964  fourierdlem81  31970  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fouriersw  32014  funcoressn  32212  usgra2pthspth  32351  idfusubc0  32591  idfusubc  32592  estrcid  32640  funcestrcsetclem5  32650  funcsetcestrclem5  32665  funcsetcestrclem7  32667  rngcval  32770  rnghmsubcsetclem1  32783  rngccat  32786  rngcid  32787  rngcidOLD  32799  rngcifuestrc  32805  funcrngcsetc  32806  funcrngcsetcALT  32807  ringcval  32816  rhmsubcsetclem1  32829  ringccat  32832  ringcid  32833  rhmsubcrngclem1  32835  rhmsubcrngc  32837  funcringcsetc  32843  funcringcsetcOLD2lem5  32848  ringcidOLD  32862  funcringcsetclem5OLD  32871  rhmsubc  32898  rhmsubcOLDlem3  32915  aacllem  33216  bnj1385  33891  bnj1326  34082  bnj1321  34083  bnj1442  34105  bnj1450  34106  bnj1463  34111  bnj1529  34126  dibffval  36867  hdmapffval  37556  hdmapfval  37557
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-opab 4511  df-xp 5010  df-res 5016
  Copyright terms: Public domain W3C validator