Theorem resabs1 5132

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 5116	. 2 |- ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2		sseqin2 3650	. . 3 |- ( B C_ C <-> ( C i^i B ) = B )
3		reseq2 5099	. . 3 |- ( ( C i^i B ) = B -> ( A |` ( C i^i B ) ) = ( A |` B ) )
4	2, 3	sylbi 199	. 2 |- ( B C_ C -> ( A |` ( C i^i B ) ) = ( A |` B ) )
5	1, 4	syl5eq 2496	1 |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Syntax hints:   -> wi 4   = wceq 1443   i^i cin 3402   C_ wss 3403   |` cres 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-xp 4839  df-rel 4840  df-res 4845

This theorem is referenced by:  resabs1d  5133  resabs2  5134  resiima  5181  fun2ssres  5622  fssres2  5749  smores3  7069  setsres  15144  gsum2dlem2  17596  lindsss  19375  resthauslem  20372  ptcmpfi  20821  tsmsres  21151  ressxms  21533  nrginvrcn  21687  xrge0gsumle  21844  lebnumii  21990  dfrelog  23508  relogf1o  23509  dvlog  23589  dvlog2  23591  efopnlem2  23595  wilthlem2  23987  gsumle  28535  rrhre  28818  iwrdsplit  29213  cvmsss2  29990  mbfposadd  31981  mzpcompact2lem  35587  eldioph2  35598  diophin  35609  diophrex  35612  2rexfrabdioph  35633  3rexfrabdioph  35634  4rexfrabdioph  35635  6rexfrabdioph  35636  7rexfrabdioph  35637  dvmptresicc  37785  fourierdlem46  38010  fourierdlem57  38021  fourierdlem111  38075  fouriersw  38089  psmeasurelem  38302