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

Theorem resabs1 4983
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 4967 . 2  |-  ( ( A  |`  C )  |`  B )  =  ( A  |`  ( C  i^i  B ) )
2 sseqin2 3389 . . 3  |-  ( B 
C_  C  <->  ( C  i^i  B )  =  B )
3 reseq2 4949 . . 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 2328 1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1628    i^i cin 3152    C_ wss 3153    |` cres 4690
This theorem is referenced by:  resabs2  4984  resiima  5028  fun2ssres  5260  fssres2  5374  fvres  5502  smores3  6365  tfrlem5  6391  setsres  13168  gsum2d  15217  ablfac1eulem  15301  resthauslem  17085  kgencn2  17246  ptcmpfi  17498  tsmsres  17820  ressxms  18065  nrginvrcn  18196  resubmet  18302  xrge0gsumle  18332  lebnumii  18458  cmsss  18766  minveclem3a  18785  dvlip2  19336  c1liplem1  19337  efcvx  19819  dfrelog  19917  relogf1o  19918  dvlog  19992  dvlog2  19994  efopnlem2  19998  logccv  20004  loglesqr  20092  wilthlem2  20301  cvmsss2  23209  cvmlift2lem9  23246  ssbnd  25911  prdsbnd2  25918  cnpwstotbnd  25920  reheibor  25962  mzpcompact2lem  26228  eldioph2  26240  diophin  26251  diophrex  26254  2rexfrabdioph  26276  3rexfrabdioph  26277  4rexfrabdioph  26278  6rexfrabdioph  26279  7rexfrabdioph  26280  fnwe2lem2  26547  lindsss  26693  dvsid  26947  afvres  27411  bnj1280  28317
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-opab 4079  df-xp 4694  df-rel 4695  df-res 4700
  Copyright terms: Public domain W3C validator