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

Theorem reseq2 5101
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 4850 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3549 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4848 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4848 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2498 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   _Vcvv 2970    i^i cin 3324    X. cxp 4834    |` cres 4838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-opab 4348  df-xp 4842  df-res 4848
This theorem is referenced by:  reseq2i  5103  reseq2d  5106  resabs1  5136  resima2  5140  imaeq2  5162  resdisj  5264  relcoi1  5363  fressnfv  5893  tfrlem1  6831  tfrlem9  6840  tfrlem11  6843  tfrlem12  6844  tfr2b  6851  tz7.44-1  6858  tz7.44-2  6859  tz7.44-3  6860  rdglem1  6867  fnfi  7585  fseqenlem1  8190  psgnprfval1  16019  gsumzaddlem  16401  gsumzaddlemOLD  16403  gsum2dlem2  16452  gsum2dOLD  16454  znunithash  17956  islinds  18197  lmbr2  18822  lmff  18864  kgencn2  19089  ptcmpfi  19345  tsmsgsum  19668  tsmsgsumOLD  19671  tsmsresOLD  19676  tsmsres  19677  tsmsf1o  19678  tsmsxplem1  19686  tsmsxp  19688  ustval  19736  xrge0gsumle  20369  xrge0tsms  20370  lmmbr2  20729  lmcau  20782  limcun  21329  jensen  22341  wilthlem2  22366  wilthlem3  22367  hhssnvt  24601  hhsssh  24605  gsumle  26181  xrge0tsmsd  26188  esumsn  26451  subfacp1lem3  27000  subfacp1lem5  27002  erdszelem1  27009  erdsze  27020  erdsze2lem2  27022  cvmscbv  27077  cvmshmeo  27090  cvmsss2  27093  ghomgrp  27238  relexpcnv  27264  rtrclreclem.min  27278  dfpo2  27494  eldm3  27501  dfrdg2  27538  nofulllem4  27775  nofulllem5  27776  mbfresfi  28363  mzpcompact2lem  29013  seff  29520
  Copyright terms: Public domain W3C validator