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

Theorem reseq2 5074
Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
Assertion
Ref Expression
reseq2  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 4825 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3478 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4823 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4823 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2437 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   _Vcvv 2892    i^i cin 3255    X. cxp 4809    |` cres 4813
This theorem is referenced by:  reseq2i  5076  reseq2d  5079  resabs1  5108  resima2  5112  imaeq2  5132  resdisj  5231  relcoi1  5331  fressnfv  5852  tfrlem9  6575  tfrlem11  6578  tfrlem12  6579  tfr2b  6586  tz7.44-1  6593  tz7.44-2  6594  tz7.44-3  6595  rdglem1  6602  fnfi  7313  fseqenlem1  7831  gsumzaddlem  15446  gsum2d  15466  znunithash  16761  lmbr2  17238  lmff  17280  kgencn2  17503  ptcmpfi  17759  tsmsgsum  18082  tsmsres  18087  tsmsf1o  18088  tsmsxplem1  18096  tsmsxp  18098  ustval  18146  xrge0gsumle  18728  xrge0tsms  18729  lmmbr2  19076  lmcau  19129  limcun  19642  jensen  20687  wilthlem2  20712  wilthlem3  20713  hhssnvt  22606  hhsssh  22610  xrge0tsmsd  24045  esumsn  24245  subfacp1lem3  24640  subfacp1lem5  24642  erdszelem1  24649  erdsze  24660  erdsze2lem2  24662  cvmscbv  24717  cvmshmeo  24730  cvmsss2  24733  ghomgrp  24873  relexpcnv  24905  rtrclreclem.min  24919  dfpo2  25129  eldm3  25136  dfrdg2  25169  nofulllem4  25376  nofulllem5  25377  mzpcompact2lem  26492  islinds  26941  seff  27200
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-in 3263  df-opab 4201  df-xp 4817  df-res 4823
  Copyright terms: Public domain W3C validator