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

Theorem reseq2 5273
Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
Assertion
Ref Expression
reseq2

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5018 . . 3
21ineq2d 3699 . 2
3 df-res 5016 . 2
4 df-res 5016 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   cvv 3109  i^icin 3474  X.cxp 5002  |`cres 5006
This theorem is referenced by:  reseq2i  5275  reseq2d  5278  resabs1  5307  resima2  5312  imaeq2  5338  resdisj  5441  relcoi1  5541  fressnfv  6085  tfrlem1  7064  tfrlem9  7073  tfrlem11  7076  tfrlem12  7077  tfr2b  7084  tz7.44-1  7091  tz7.44-2  7092  tz7.44-3  7093  rdglem1  7100  fnfi  7818  fseqenlem1  8426  psgnprfval1  16547  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsum2dlem2  16998  gsum2dOLD  17000  znunithash  18603  islinds  18844  lmbr2  19760  lmff  19802  kgencn2  20058  ptcmpfi  20314  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsxplem1  20655  tsmsxp  20657  ustval  20705  xrge0gsumle  21338  xrge0tsms  21339  lmmbr2  21698  lmcau  21751  limcun  22299  jensen  23318  wilthlem2  23343  wilthlem3  23344  hhssnvt  26181  hhsssh  26185  foresf1o  27403  gsumle  27770  xrge0tsmsd  27775  esumsn  28072  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem1  28635  erdsze  28646  erdsze2lem2  28648  cvmscbv  28703  cvmshmeo  28716  cvmsss2  28719  ghomgrp  29030  relexpcnv  29056  rtrclreclem.min  29070  dfpo2  29184  eldm3  29191  dfrdg2  29228  nofulllem4  29465  nofulllem5  29466  mbfresfi  30061  mzpcompact2lem  30684  seff  31189  fouriersw  32014
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