Theorem resabs1 5848

Description: Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.)

Assertion

Ref	Expression
resabs1	⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Proof of Theorem resabs1

Step	Hyp	Ref	Expression
1		resres 5831	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4142	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5813	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 220	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	syl5eq 2845	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1538   ∩ cin 3880   ⊆ wss 3881   ↾ cres 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526  df-res 5531

This theorem is referenced by:  resabs1d  5849  resabs2  5850  resiima  5911  fun2ssres  6369  fssres2  6520  smores3  7973  setsres  16517  gsum2dlem2  19084  lindsss  20513  resthauslem  21968  ptcmpfi  22418  tsmsres  22749  ressxms  23132  nrginvrcn  23298  xrge0gsumle  23438  lebnumii  23571  dvmptresicc  24519  dfrelog  25157  relogf1o  25158  dvlog  25242  dvlog2  25244  efopnlem2  25248  wilthlem2  25654  gsumle  30775  rrhre  31372  iwrdsplit  31755  rpsqrtcn  31974  pthhashvtx  32487  cvmsss2  32634  nosupres  33320  nosupbnd2lem1  33328  mbfposadd  35104  mzpcompact2lem  39692  eldioph2  39703  diophin  39713  diophrex  39716  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  resabs1i  41782  fourierdlem46  42794  fourierdlem57  42805  fourierdlem111  42859  fouriersw  42873  psmeasurelem  43109