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

Theorem reseq2 5057
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 4805 . . 3  |-  ( A  =  B  ->  ( A  X.  _V )  =  ( B  X.  _V ) )
21ineq2d 3602 . 2  |-  ( A  =  B  ->  ( C  i^i  ( A  X.  _V ) )  =  ( C  i^i  ( B  X.  _V ) ) )
3 df-res 4803 . 2  |-  ( C  |`  A )  =  ( C  i^i  ( A  X.  _V ) )
4 df-res 4803 . 2  |-  ( C  |`  B )  =  ( C  i^i  ( B  X.  _V ) )
52, 3, 43eqtr4g 2482 1  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   _Vcvv 3017    i^i cin 3373    X. cxp 4789    |` cres 4793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381  df-opab 4421  df-xp 4797  df-res 4803
This theorem is referenced by:  reseq2i  5059  reseq2d  5062  resabs1  5090  resima2  5095  imaeq2  5121  resdisj  5223  relcoi1OLD  5322  fressnfv  6032  tfrlem1  7044  tfrlem9  7053  tfrlem11  7056  tfrlem12  7057  tfr2b  7064  tz7.44-1  7074  tz7.44-2  7075  tz7.44-3  7076  rdglem1  7083  fnfi  7797  fseqenlem1  8401  rtrclreclem4  13063  psgnprfval1  17101  gsumzaddlem  17492  gsum2dlem2  17541  znunithash  19072  islinds  19304  lmbr2  20212  lmff  20254  kgencn2  20509  ptcmpfi  20765  tsmsgsum  21090  tsmsres  21095  tsmsf1o  21096  tsmsxplem1  21104  tsmsxp  21106  ustval  21154  xrge0gsumle  21788  xrge0tsms  21789  lmmbr2  22166  lmcau  22219  limcun  22787  jensen  23851  wilthlem2  23931  wilthlem3  23932  hhssnvt  26853  hhsssh  26857  foresf1o  28077  gsumle  28488  xrge0tsmsd  28495  esumsnf  28832  subfacp1lem3  29852  subfacp1lem5  29854  erdszelem1  29861  erdsze  29872  erdsze2lem2  29874  cvmscbv  29928  cvmshmeo  29941  cvmsss2  29944  ghomgrp  30255  dfpo2  30341  eldm3  30348  dfrdg2  30388  nofulllem4  30538  nofulllem5  30539  mbfresfi  31894  mzpcompact2lem  35505  seff  36570  wessf1ornlem  37363  fouriersw  37978  sge0tsms  38073  sge0f1o  38075  sge0sup  38084  meadjuni  38146  ismeannd  38156  psmeasurelem  38159  psmeasure  38160  omeunile  38177  isomennd  38203  hoidmvlelem3  38266  egrsubgr  39086
  Copyright terms: Public domain W3C validator