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

Theorem reseq1 5277
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 3689 . 2  |-  ( A  =  B  ->  ( A  i^i  ( C  X.  _V ) )  =  ( B  i^i  ( C  X.  _V ) ) )
2 df-res 5020 . 2  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
3 df-res 5020 . 2  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
41, 2, 33eqtr4g 2523 1  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395   _Vcvv 3109    i^i cin 3470    X. cxp 5006    |` cres 5010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-res 5020
This theorem is referenced by:  reseq1i  5279  reseq1d  5282  imaeq1  5342  relcoi1  5542  fvtresfn  5957  tfrlem12  7076  pmresg  7465  resixpfo  7526  mapunen  7705  fseqenlem1  8422  axdc3lem2  8848  axdc3lem4  8850  axdc  8918  hashf1lem1  12507  lo1eq  13402  rlimeq  13403  symgfixfo  16590  lspextmo  17828  evlseu  18311  mdetunilem3  19242  mdetunilem4  19243  mdetunilem9  19248  lmbr  19885  ptuncnv  20433  iscau  21840  plyexmo  22834  relogf1o  23079  isdivrngo  25559  eulerpartlemt  28485  eulerpartlemgv  28487  eulerpartlemn  28495  eulerpart  28496  iscvm  28879  ghomgrplem  29204  trpredlem1  29484  trpredtr  29487  trpredmintr  29488  wfrlem1  29517  wfrlem15  29531  frrlem1  29561  nofulllem5  29640  mbfresfi  30223  eqfnun  30374  sdclem2  30397  mzpcompact2lem  30846  diophrw  30854  eldioph2lem1  30855  eldioph2lem2  30856  eldioph3  30861  diophin  30868  diophrex  30871  rexrabdioph  30889  2rexfrabdioph  30891  3rexfrabdioph  30892  4rexfrabdioph  30893  6rexfrabdioph  30894  7rexfrabdioph  30895  eldioph4b  30907  pwssplit4  31197  dvnprodlem1  31904  dvnprodlem3  31906  bnj1385  33992  bnj66  34019  bnj1234  34170  bnj1326  34183  bnj1463  34212
  Copyright terms: Public domain W3C validator