Theorem resabs1 5121

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 5105	. 2 |- ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2		sseqin2 3657	. . 3 |- ( B C_ C <-> ( C i^i B ) = B )
3		reseq2 5088	. . 3 |- ( ( C i^i B ) = B -> ( A |` ( C i^i B ) ) = ( A |` B ) )
4	2, 3	sylbi 195	. 2 |- ( B C_ C -> ( A |` ( C i^i B ) ) = ( A |` B ) )
5	1, 4	syl5eq 2455	1 |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Syntax hints:   -> wi 4   = wceq 1405   i^i cin 3412   C_ wss 3413   |` cres 4824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453  df-xp 4828  df-rel 4829  df-res 4834

This theorem is referenced by:  resabs1d  5122  resabs2  5123  resiima  5170  fun2ssres  5609  fssres2  5735  smores3  7056  setsres  14869  gsum2dlem2  17317  gsum2dOLD  17319  lindsss  19149  resthauslem  20155  ptcmpfi  20604  tsmsresOLD  20935  tsmsres  20936  ressxms  21318  nrginvrcn  21490  xrge0gsumle  21628  lebnumii  21756  dfrelog  23243  relogf1o  23244  dvlog  23324  dvlog2  23326  efopnlem2  23330  wilthlem2  23722  gsumle  28207  rrhre  28437  iwrdsplit  28818  cvmsss2  29558  mbfposadd  31414  mzpcompact2lem  35025  eldioph2  35036  diophin  35047  diophrex  35050  2rexfrabdioph  35071  3rexfrabdioph  35072  4rexfrabdioph  35073  6rexfrabdioph  35074  7rexfrabdioph  35075  dvmptresicc  37065  fourierdlem46  37284  fourierdlem57  37295  fourierdlem111  37349  fouriersw  37363