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

Theorem reseq1 5140
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 3535 . 2  |-  ( A  =  B  ->  ( A  i^i  ( C  X.  _V ) )  =  ( B  i^i  ( C  X.  _V ) ) )
2 df-res 4890 . 2  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
3 df-res 4890 . 2  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
41, 2, 33eqtr4g 2493 1  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   _Vcvv 2956    i^i cin 3319    X. cxp 4876    |` cres 4880
This theorem is referenced by:  reseq1i  5142  reseq1d  5145  imaeq1  5198  relcoi1  5398  tfrlem3  6638  tfrlem3a  6639  tfrlem12  6650  pmresg  7041  resixpfo  7100  mapunen  7276  fseqenlem1  7905  axdc3lem2  8331  axdc3lem4  8333  axdc  8401  hashf1lem1  11704  lo1eq  12362  rlimeq  12363  lspextmo  16132  lmbr  17322  ptuncnv  17839  iscau  19229  evlseu  19937  plyexmo  20230  relogf1o  20464  isdivrngo  22019  iscvm  24946  ghomgrplem  25100  trpredlem1  25505  trpredtr  25508  trpredmintr  25509  wfrlem1  25538  wfrlem15  25552  frrlem1  25582  nofulllem5  25661  mbfresfi  26253  eqfnun  26423  sdclem2  26446  fvtresfn  26744  mzpcompact2lem  26808  diophrw  26817  eldioph2lem1  26818  eldioph2lem2  26819  eldioph3  26824  diophin  26831  diophrex  26834  rexrabdioph  26854  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  eldioph4b  26872  pwssplit4  27168  bnj1385  29204  bnj66  29231  bnj1234  29382  bnj1326  29395  bnj1463  29424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-res 4890
  Copyright terms: Public domain W3C validator