Theorem resabs1 5139

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

Step	Hyp	Ref	Expression
1		resres 5123	. 2 |- ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2		sseqin2 3642	. . 3 |- ( B C_ C <-> ( C i^i B ) = B )
3		reseq2 5106	. . 3 |- ( ( C i^i B ) = B -> ( A |` ( C i^i B ) ) = ( A |` B ) )
4	2, 3	sylbi 200	. 2 |- ( B C_ C -> ( A |` ( C i^i B ) ) = ( A |` B ) )
5	1, 4	syl5eq 2517	1 |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Syntax hints:   -> wi 4   = wceq 1452   i^i cin 3389   C_ wss 3390   |` cres 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-opab 4455  df-xp 4845  df-rel 4846  df-res 4851

This theorem is referenced by:  resabs1d  5140  resabs2  5141  resiima  5188  fun2ssres  5630  fssres2  5763  smores3  7090  setsres  15229  gsum2dlem2  17681  lindsss  19459  resthauslem  20456  ptcmpfi  20905  tsmsres  21236  ressxms  21618  nrginvrcn  21772  xrge0gsumle  21929  lebnumii  22075  dfrelog  23594  relogf1o  23595  dvlog  23675  dvlog2  23677  efopnlem2  23681  wilthlem2  24073  gsumle  28616  rrhre  28899  iwrdsplit  29293  cvmsss2  30069  mbfposadd  32052  mzpcompact2lem  35664  eldioph2  35675  diophin  35686  diophrex  35689  2rexfrabdioph  35710  3rexfrabdioph  35711  4rexfrabdioph  35712  6rexfrabdioph  35713  7rexfrabdioph  35714  dvmptresicc  37888  fourierdlem46  38128  fourierdlem57  38139  fourierdlem111  38193  fouriersw  38207  psmeasurelem  38424