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

Theorem resabs1 4984
Description: Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)
Assertion
Ref Expression
resabs1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)

Proof of Theorem resabs1
StepHypRef Expression
1 resres 4968 . 2  |-  ( ( A  |`  C )  |`  B )  =  ( A  |`  ( C  i^i  B ) )
2 sseqin2 3388 . . 3  |-  ( B 
C_  C  <->  ( C  i^i  B )  =  B )
3 reseq2 4950 . . 3  |-  ( ( C  i^i  B )  =  B  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
42, 3sylbi 187 . 2  |-  ( B 
C_  C  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
51, 4syl5eq 2327 1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    i^i cin 3151    C_ wss 3152    |` cres 4691
This theorem is referenced by:  resabs2  4985  resiima  5029  fun2ssres  5295  fssres2  5409  smores3  6370  tfrlem5  6396  setsres  13174  gsum2d  15223  ablfac1eulem  15307  resthauslem  17091  kgencn2  17252  ptcmpfi  17504  tsmsres  17826  ressxms  18071  nrginvrcn  18202  resubmet  18308  xrge0gsumle  18338  lebnumii  18464  cmsss  18772  minveclem3a  18791  dvlip2  19342  c1liplem1  19343  efcvx  19825  dfrelog  19923  relogf1o  19924  dvlog  19998  dvlog2  20000  efopnlem2  20004  logccv  20010  loglesqr  20098  wilthlem2  20307  cvmsss2  23805  cvmlift2lem9  23842  ssbnd  26512  prdsbnd2  26519  cnpwstotbnd  26521  reheibor  26563  mzpcompact2lem  26829  eldioph2  26841  diophin  26852  diophrex  26855  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  fnwe2lem2  27148  lindsss  27294  dvsid  27548  afvres  28034  bnj1280  29050
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-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  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-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-rel 4696  df-res 4701
  Copyright terms: Public domain W3C validator