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

Theorem resabs1 5166
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 5150 . 2  |-  ( ( A  |`  C )  |`  B )  =  ( A  |`  ( C  i^i  B ) )
2 sseqin2 3552 . . 3  |-  ( B 
C_  C  <->  ( C  i^i  B )  =  B )
3 reseq2 5132 . . 3  |-  ( ( C  i^i  B )  =  B  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
42, 3sylbi 188 . 2  |-  ( B 
C_  C  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
51, 4syl5eq 2479 1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    i^i cin 3311    C_ wss 3312    |` cres 4871
This theorem is referenced by:  resabs2  5167  resiima  5211  fun2ssres  5485  fssres2  5602  f2ndf  6443  smores3  6606  tfrlem5  6632  setsres  13483  gsum2d  15534  ablfac1eulem  15618  resthauslem  17415  kgencn2  17577  ptcmpfi  17833  tsmsres  18161  ressxms  18543  nrginvrcn  18715  resubmet  18821  xrge0gsumle  18852  lebnumii  18979  cmsss  19291  minveclem3a  19316  dvlip2  19867  c1liplem1  19868  efcvx  20353  dfrelog  20451  relogf1o  20452  dvlog  20530  dvlog2  20532  efopnlem2  20536  logccv  20542  loglesqr  20630  wilthlem2  20840  rrhre  24375  cvmsss2  24949  cvmlift2lem9  24986  mbfresfi  26199  mbfposadd  26200  ssbnd  26434  prdsbnd2  26441  cnpwstotbnd  26443  reheibor  26485  mzpcompact2lem  26745  eldioph2  26757  diophin  26768  diophrex  26771  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  fnwe2lem2  27063  lindsss  27209  dvsid  27463  afvres  27950  bnj1280  29243
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-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-opab 4259  df-xp 4875  df-rel 4876  df-res 4881
  Copyright terms: Public domain W3C validator