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

Theorem reseq2 5110
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 4859 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3557 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4857 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4857 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2500 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   _Vcvv 2977    i^i cin 3332    X. cxp 4843    |` cres 4847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-opab 4356  df-xp 4851  df-res 4857
This theorem is referenced by:  reseq2i  5112  reseq2d  5115  resabs1  5144  resima2  5148  imaeq2  5170  resdisj  5272  relcoi1  5371  fressnfv  5901  tfrlem1  6840  tfrlem9  6849  tfrlem11  6852  tfrlem12  6853  tfr2b  6860  tz7.44-1  6867  tz7.44-2  6868  tz7.44-3  6869  rdglem1  6876  fnfi  7594  fseqenlem1  8199  psgnprfval1  16031  gsumzaddlem  16413  gsumzaddlemOLD  16415  gsum2dlem2  16467  gsum2dOLD  16469  znunithash  18002  islinds  18243  lmbr2  18868  lmff  18910  kgencn2  19135  ptcmpfi  19391  tsmsgsum  19714  tsmsgsumOLD  19717  tsmsresOLD  19722  tsmsres  19723  tsmsf1o  19724  tsmsxplem1  19732  tsmsxp  19734  ustval  19782  xrge0gsumle  20415  xrge0tsms  20416  lmmbr2  20775  lmcau  20828  limcun  21375  jensen  22387  wilthlem2  22412  wilthlem3  22413  hhssnvt  24671  hhsssh  24675  gsumle  26251  xrge0tsmsd  26258  esumsn  26520  subfacp1lem3  27075  subfacp1lem5  27077  erdszelem1  27084  erdsze  27095  erdsze2lem2  27097  cvmscbv  27152  cvmshmeo  27165  cvmsss2  27168  ghomgrp  27314  relexpcnv  27340  rtrclreclem.min  27354  dfpo2  27570  eldm3  27577  dfrdg2  27614  nofulllem4  27851  nofulllem5  27852  mbfresfi  28443  mzpcompact2lem  29093  seff  29600
  Copyright terms: Public domain W3C validator