Theorem resabs1 5127

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 5111	. 2 |- ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2		sseqin2 3557	. . 3 |- ( B C_ C <-> ( C i^i B ) = B )
3		reseq2 5092	. . 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 2477	1 |- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Syntax hints:   -> wi 4   = wceq 1362   i^i cin 3315   C_ wss 3316   |` cres 4829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-opab 4339  df-xp 4833  df-rel 4834  df-res 4839

This theorem is referenced by:  resabs2  5128  resiima  5171  fun2ssres  5447  fssres2  5567  f2ndf  6667  smores3  6800  setsres  14185  gsum2dlem2  16436  gsum2dOLD  16438  ablfac1eulem  16547  lindsss  18095  resthauslem  18809  kgencn2  18972  ptcmpfi  19228  tsmsresOLD  19559  tsmsres  19560  ressxms  19942  nrginvrcn  20114  resubmet  20221  xrge0gsumle  20252  lebnumii  20380  cmsss  20703  minveclem3a  20756  dvlip2  21309  c1liplem1  21310  efcvx  21799  dfrelog  21902  relogf1o  21903  dvlog  21981  dvlog2  21983  efopnlem2  21987  logccv  21993  loglesqr  22081  wilthlem2  22292  gsumle  26098  rrhre  26301  iwrdsplit  26618  cvmsss2  27011  cvmlift2lem9  27048  mbfresfi  28282  mbfposadd  28283  ssbnd  28531  prdsbnd2  28538  cnpwstotbnd  28540  reheibor  28582  mzpcompact2lem  28933  eldioph2  28945  diophin  28956  diophrex  28959  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  fnwe2lem2  29249  dvsid  29450  afvres  29924  bnj1280  31734