Theorem resabs1 6003

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 5989	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4184	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5971	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 220	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2816	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1567   ∩ cin 3912   ⊆ wss 3913   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5175  df-xp 5665  df-rel 5666  df-res 5671

This theorem is referenced by:  resabs1i  6004  resabs1d  6005  resabs2  6006  resiima  6076  fun2ssres  6578  fssres2  6744  smores3  8336  setsres  17234  gsum2dlem2  20037  gsumle  20211  lindsss  21939  resthauslem  23485  ptcmpfi  23935  tsmsres  24266  ressxms  24647  nrginvrcn  24814  xrge0gsumle  24956  lebnumii  25090  dvmptresicc  26040  dfrelog  26692  relogf1o  26693  dvlog  26778  dvlog2  26780  efopnlem2  26784  wilthlem2  27195  nosupres  27833  nosupbnd2lem1  27841  noinfres  27848  noinfbnd2lem1  27856  nosupinfsep  27858  rrhre  34352  iwrdsplit  34718  rpsqrtcn  34921  pthhashvtx  35515  cvmsss2  35661  mbfposadd  38201  mzpcompact2lem  43367  eldioph2  43378  diophin  43388  diophrex  43391  2rexfrabdioph  43408  3rexfrabdioph  43409  4rexfrabdioph  43410  6rexfrabdioph  43411  7rexfrabdioph  43412  fourierdlem46  46751  fourierdlem57  46762  fourierdlem111  46816  fouriersw  46830  psmeasurelem  47069