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

Theorem resabs1 4958
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 4942 . 2  |-  ( ( A  |`  C )  |`  B )  =  ( A  |`  ( C  i^i  B ) )
2 sseqin2 3349 . . 3  |-  ( B 
C_  C  <->  ( C  i^i  B )  =  B )
3 reseq2 4924 . . 3  |-  ( ( C  i^i  B )  =  B  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
42, 3sylbi 189 . 2  |-  ( B 
C_  C  ->  ( A  |`  ( C  i^i  B ) )  =  ( A  |`  B )
)
51, 4syl5eq 2300 1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    i^i cin 3112    C_ wss 3113    |` cres 4649
This theorem is referenced by:  resabs2  4959  resiima  5003  fun2ssres  5219  fssres2  5333  fvres  5461  smores3  6324  tfrlem5  6350  setsres  13122  gsum2d  15171  ablfac1eulem  15255  resthauslem  17039  kgencn2  17200  ptcmpfi  17452  tsmsres  17774  ressxms  18019  nrginvrcn  18150  resubmet  18256  xrge0gsumle  18286  lebnumii  18412  cmsss  18720  minveclem3a  18739  dvlip2  19290  c1liplem1  19291  efcvx  19773  dfrelog  19871  relogf1o  19872  dvlog  19946  dvlog2  19948  efopnlem2  19952  logccv  19958  loglesqr  20046  wilthlem2  20255  cvmsss2  23163  cvmlift2lem9  23200  ssbnd  25865  prdsbnd2  25872  cnpwstotbnd  25874  reheibor  25916  mzpcompact2lem  26182  eldioph2  26194  diophin  26205  diophrex  26208  2rexfrabdioph  26230  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  fnwe2lem2  26501  lindsss  26647  dvsid  26901  bnj1280  28083
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-opab 4038  df-xp 4661  df-rel 4662  df-res 4667
  Copyright terms: Public domain W3C validator