Theorem resabs1 5300

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 5284	. 2 |- ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2		sseqin2 3717	. . 3 |- ( B C_ C <-> ( C i^i B ) = B )
3		reseq2 5266	. . 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 2520	1 |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Syntax hints:   -> wi 4   = wceq 1379   i^i cin 3475   C_ wss 3476   |` cres 5001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-xp 5005  df-rel 5006  df-res 5011

This theorem is referenced by:  resabs1d  5301  resabs2  5302  resiima  5349  fun2ssres  5627  fssres2  5751  f2ndf  6886  smores3  7021  setsres  14514  gsum2dlem2  16789  gsum2dOLD  16791  ablfac1eulem  16913  lindsss  18626  resthauslem  19630  kgencn2  19793  ptcmpfi  20049  tsmsresOLD  20380  tsmsres  20381  ressxms  20763  nrginvrcn  20935  resubmet  21042  xrge0gsumle  21073  lebnumii  21201  cmsss  21524  minveclem3a  21577  dvlip2  22131  c1liplem1  22132  efcvx  22578  dfrelog  22681  relogf1o  22682  dvlog  22760  dvlog2  22762  efopnlem2  22766  logccv  22772  loglesqrt  22860  wilthlem2  23071  gsumle  27433  rrhre  27635  iwrdsplit  27966  cvmsss2  28359  cvmlift2lem9  28396  mbfresfi  29638  mbfposadd  29639  ssbnd  29887  prdsbnd2  29894  cnpwstotbnd  29896  reheibor  29938  mzpcompact2lem  30288  eldioph2  30299  diophin  30310  diophrex  30313  2rexfrabdioph  30333  3rexfrabdioph  30334  4rexfrabdioph  30335  6rexfrabdioph  30336  7rexfrabdioph  30337  fnwe2lem2  30601  dvsid  30836  dvmptresicc  31249  fourierdlem46  31453  fourierdlem48  31455  fourierdlem49  31456  fourierdlem57  31464  fourierdlem58  31465  fourierdlem72  31479  fourierdlem75  31482  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem93  31500  fourierdlem100  31507  fourierdlem103  31510  fourierdlem104  31511  fourierdlem107  31514  fourierdlem111  31518  fourierdlem112  31519  fouriersw  31532  afvres  31724  bnj1280  33155