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

Theorem reseq1 4965
Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
reseq1  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 3376 . 2  |-  ( A  =  B  ->  ( A  i^i  ( C  X.  _V ) )  =  ( B  i^i  ( C  X.  _V ) ) )
2 df-res 4717 . 2  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
3 df-res 4717 . 2  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
41, 2, 33eqtr4g 2353 1  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
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:  reseq1i  4967  reseq1d  4970  imaeq1  5023  relcoi1  5217  tfrlem3  6409  tfrlem3a  6410  tfrlem12  6421  pmresg  6811  resixpfo  6870  mapunen  7046  fseqenlem1  7667  axdc3lem2  8093  axdc3lem4  8095  axdc  8164  hashf1lem1  11409  lo1eq  12058  rlimeq  12059  lspextmo  15829  lmbr  17004  ptuncnv  17514  iscau  18718  evlseu  19416  plyexmo  19709  relogf1o  19940  isdivrngo  21114  iscvm  23805  ghomgrplem  24011  trpredlem1  24301  trpredtr  24304  trpredmintr  24305  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  nofulllem5  24431  bpolyval  24856  eqfnung2  25221  prjmapcp2  25273  eqfnun  26490  sdclem2  26555  fvtresfn  26866  mzpcompact2lem  26932  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  eldioph3  26948  diophin  26955  diophrex  26958  rexrabdioph  26978  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  eldioph4b  26997  pwssplit4  27294  bnj1385  29181  bnj66  29208  bnj1234  29359  bnj1326  29372  bnj1463  29401
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-res 4717
  Copyright terms: Public domain W3C validator