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

Theorem reseq2 5266
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 5013 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3700 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 5011 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 5011 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2533 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   _Vcvv 3113    i^i cin 3475    X. cxp 4997    |` cres 5001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-opab 4506  df-xp 5005  df-res 5011
This theorem is referenced by:  reseq2i  5268  reseq2d  5271  resabs1  5300  resima2  5305  imaeq2  5331  resdisj  5434  relcoi1  5534  fressnfv  6073  tfrlem1  7042  tfrlem9  7051  tfrlem11  7054  tfrlem12  7055  tfr2b  7062  tz7.44-1  7069  tz7.44-2  7070  tz7.44-3  7071  rdglem1  7078  fnfi  7794  fseqenlem1  8401  psgnprfval1  16343  gsumzaddlem  16725  gsumzaddlemOLD  16727  gsum2dlem2  16789  gsum2dOLD  16791  znunithash  18370  islinds  18611  lmbr2  19526  lmff  19568  kgencn2  19793  ptcmpfi  20049  tsmsgsum  20372  tsmsgsumOLD  20375  tsmsresOLD  20380  tsmsres  20381  tsmsf1o  20382  tsmsxplem1  20390  tsmsxp  20392  ustval  20440  xrge0gsumle  21073  xrge0tsms  21074  lmmbr2  21433  lmcau  21486  limcun  22034  jensen  23046  wilthlem2  23071  wilthlem3  23072  hhssnvt  25857  hhsssh  25861  gsumle  27433  xrge0tsmsd  27438  esumsn  27712  subfacp1lem3  28266  subfacp1lem5  28268  erdszelem1  28275  erdsze  28286  erdsze2lem2  28288  cvmscbv  28343  cvmshmeo  28356  cvmsss2  28359  ghomgrp  28505  relexpcnv  28531  rtrclreclem.min  28545  dfpo2  28761  eldm3  28768  dfrdg2  28805  nofulllem4  29042  nofulllem5  29043  mbfresfi  29638  mzpcompact2lem  30288  seff  30792  fouriersw  31532
  Copyright terms: Public domain W3C validator