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

Theorem reseq2 5134
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 4885 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3535 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4883 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4883 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2493 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   _Vcvv 2949    i^i cin 3312    X. cxp 4869    |` cres 4873
This theorem is referenced by:  reseq2i  5136  reseq2d  5139  resabs1  5168  resima2  5172  imaeq2  5192  resdisj  5291  relcoi1  5391  fressnfv  5913  tfrlem9  6639  tfrlem11  6642  tfrlem12  6643  tfr2b  6650  tz7.44-1  6657  tz7.44-2  6658  tz7.44-3  6659  rdglem1  6666  fnfi  7377  fseqenlem1  7898  gsumzaddlem  15519  gsum2d  15539  znunithash  16838  lmbr2  17316  lmff  17358  kgencn2  17582  ptcmpfi  17838  tsmsgsum  18161  tsmsres  18166  tsmsf1o  18167  tsmsxplem1  18175  tsmsxp  18177  ustval  18225  xrge0gsumle  18857  xrge0tsms  18858  lmmbr2  19205  lmcau  19258  limcun  19775  jensen  20820  wilthlem2  20845  wilthlem3  20846  hhssnvt  22758  hhsssh  22762  xrge0tsmsd  24216  esumsn  24449  subfacp1lem3  24861  subfacp1lem5  24863  erdszelem1  24870  erdsze  24881  erdsze2lem2  24883  cvmscbv  24938  cvmshmeo  24951  cvmsss2  24954  ghomgrp  25094  relexpcnv  25126  rtrclreclem.min  25140  dfpo2  25371  eldm3  25378  dfrdg2  25416  nofulllem4  25653  nofulllem5  25654  mbfresfi  26244  mzpcompact2lem  26800  islinds  27248  seff  27507
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-in 3320  df-opab 4260  df-xp 4877  df-res 4883
  Copyright terms: Public domain W3C validator