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

Theorem reseq1 4949
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 3363 . 2  |-  ( A  =  B  ->  ( A  i^i  ( C  X.  _V ) )  =  ( B  i^i  ( C  X.  _V ) ) )
2 df-res 4701 . 2  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
3 df-res 4701 . 2  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
41, 2, 33eqtr4g 2340 1  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
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:  reseq1i  4951  reseq1d  4954  imaeq1  5007  relcoi1  5201  tfrlem3  6393  tfrlem3a  6394  tfrlem12  6405  pmresg  6795  resixpfo  6854  mapunen  7030  fseqenlem1  7651  axdc3lem2  8077  axdc3lem4  8079  axdc  8148  hashf1lem1  11393  lo1eq  12042  rlimeq  12043  lspextmo  15813  lmbr  16988  ptuncnv  17498  iscau  18702  evlseu  19400  plyexmo  19693  relogf1o  19924  isdivrngo  21098  iscvm  23790  ghomgrplem  23996  trpredlem1  24230  trpredtr  24233  trpredmintr  24234  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  nofulllem5  24360  bpolyval  24784  eqfnung2  25118  prjmapcp2  25170  eqfnun  26387  sdclem2  26452  fvtresfn  26763  mzpcompact2lem  26829  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  eldioph3  26845  diophin  26852  diophrex  26855  rexrabdioph  26875  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  eldioph4b  26894  pwssplit4  27191  bnj1385  28865  bnj66  28892  bnj1234  29043  bnj1326  29056  bnj1463  29085
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-res 4701
  Copyright terms: Public domain W3C validator