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

Theorem resabs1 5000
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 4984 . 2  |-  ( ( A  |`  C )  |`  B )  =  ( A  |`  ( C  i^i  B ) )
2 sseqin2 3401 . . 3  |-  ( B 
C_  C  <->  ( C  i^i  B )  =  B )
3 reseq2 4966 . . 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 2340 1  |-  ( B 
C_  C  ->  (
( A  |`  C )  |`  B )  =  ( A  |`  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    i^i cin 3164    C_ wss 3165    |` cres 4707
This theorem is referenced by:  resabs2  5001  resiima  5045  fun2ssres  5311  fssres2  5425  smores3  6386  tfrlem5  6412  setsres  13190  gsum2d  15239  ablfac1eulem  15323  resthauslem  17107  kgencn2  17268  ptcmpfi  17520  tsmsres  17842  ressxms  18087  nrginvrcn  18218  resubmet  18324  xrge0gsumle  18354  lebnumii  18480  cmsss  18788  minveclem3a  18807  dvlip2  19358  c1liplem1  19359  efcvx  19841  dfrelog  19939  relogf1o  19940  dvlog  20014  dvlog2  20016  efopnlem2  20020  logccv  20026  loglesqr  20114  wilthlem2  20323  cvmsss2  23820  cvmlift2lem9  23857  ssbnd  26615  prdsbnd2  26622  cnpwstotbnd  26624  reheibor  26666  mzpcompact2lem  26932  eldioph2  26944  diophin  26955  diophrex  26958  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  fnwe2lem2  27251  lindsss  27397  dvsid  27651  afvres  28140  bnj1280  29366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-xp 4711  df-rel 4712  df-res 4717
  Copyright terms: Public domain W3C validator