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

Theorem reseq2 4966
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 4719 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3383 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4717 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4717 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   _Vcvv 2801    i^i cin 3164    X. cxp 4703    |` cres 4707
This theorem is referenced by:  reseq2i  4968  reseq2d  4971  resabs1  5000  resima2  5004  imaeq2  5024  resdisj  5121  relcoi1  5217  fressnfv  5723  tfrlem9  6417  tfrlem11  6420  tfrlem12  6421  tfr2b  6428  tz7.44-1  6435  tz7.44-2  6436  tz7.44-3  6437  rdglem1  6444  fnfi  7150  fseqenlem1  7667  gsumzaddlem  15219  gsum2d  15239  znunithash  16534  lmbr2  17005  lmff  17045  kgencn2  17268  ptcmpfi  17520  tsmsgsum  17837  tsmsres  17842  tsmsf1o  17843  tsmsxplem1  17851  tsmsxp  17853  xrge0gsumle  18354  xrge0tsms  18355  lmmbr2  18701  lmcau  18754  limcun  19261  jensen  20299  wilthlem2  20323  wilthlem3  20324  hhssnvt  21858  hhsssh  21862  xrge0tsmsd  23397  esumsn  23452  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem1  23737  erdsze  23748  erdsze2lem2  23750  cvmscbv  23804  cvmshmeo  23817  cvmsss2  23820  ghomgrp  24012  relexpcnv  24044  rtrclreclem.min  24059  dfpo2  24183  eldm3  24190  dfrdg2  24223  nofulllem4  24430  nofulllem5  24431  scprefat  25174  scprefat2  25175  isprj1  25266  preoref22  25332  dfps2  25392  valtar  25986  idmor  26049  mzpcompact2lem  26932  islinds  27382  seff  27641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-opab 4094  df-xp 4711  df-res 4717
  Copyright terms: Public domain W3C validator