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

Theorem reseq2 4950
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 4703 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3370 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4701 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4701 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   _Vcvv 2788    i^i cin 3151    X. cxp 4687    |` cres 4691
This theorem is referenced by:  reseq2i  4952  reseq2d  4955  resabs1  4984  resima2  4988  imaeq2  5008  resdisj  5105  relcoi1  5201  fressnfv  5707  tfrlem9  6401  tfrlem11  6404  tfrlem12  6405  tfr2b  6412  tz7.44-1  6419  tz7.44-2  6420  tz7.44-3  6421  rdglem1  6428  fnfi  7134  fseqenlem1  7651  gsumzaddlem  15203  gsum2d  15223  znunithash  16518  lmbr2  16989  lmff  17029  kgencn2  17252  ptcmpfi  17504  tsmsgsum  17821  tsmsres  17826  tsmsf1o  17827  tsmsxplem1  17835  tsmsxp  17837  xrge0gsumle  18338  xrge0tsms  18339  lmmbr2  18685  lmcau  18738  limcun  19245  jensen  20283  wilthlem2  20307  wilthlem3  20308  hhssnvt  21842  hhsssh  21846  xrge0tsmsd  23382  esumsn  23437  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem1  23722  erdsze  23733  erdsze2lem2  23735  cvmscbv  23789  cvmshmeo  23802  cvmsss2  23805  ghomgrp  23997  relexpcnv  24029  rtrclreclem.min  24044  dfpo2  24112  eldm3  24119  dfrdg2  24152  nofulllem4  24359  nofulllem5  24360  scprefat  25071  scprefat2  25072  isprj1  25163  preoref22  25229  dfps2  25289  valtar  25883  idmor  25946  mzpcompact2lem  26829  islinds  27279  seff  27538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator