Theorem resabs1 6027

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 6013	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4231	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5995	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 217	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2787	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3962   ⊆ wss 3963   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-xp 5695  df-rel 5696  df-res 5701

This theorem is referenced by:  resabs1d  6028  resabs2  6029  resiima  6096  fun2ssres  6613  fssres2  6777  smores3  8392  setsres  17212  gsum2dlem2  20004  lindsss  21862  resthauslem  23387  ptcmpfi  23837  tsmsres  24168  ressxms  24554  nrginvrcn  24729  xrge0gsumle  24869  lebnumii  25012  dvmptresicc  25966  dfrelog  26622  relogf1o  26623  dvlog  26708  dvlog2  26710  efopnlem2  26714  wilthlem2  27127  nosupres  27767  nosupbnd2lem1  27775  noinfres  27782  noinfbnd2lem1  27790  nosupinfsep  27792  gsumle  33084  rrhre  33984  iwrdsplit  34369  rpsqrtcn  34587  pthhashvtx  35112  cvmsss2  35259  mbfposadd  37654  mzpcompact2lem  42739  eldioph2  42750  diophin  42760  diophrex  42763  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  resabs1i  45085  fourierdlem46  46108  fourierdlem57  46119  fourierdlem111  46173  fouriersw  46187  psmeasurelem  46426