Theorem resabs1 5993

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3925   ⊆ wss 3926   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660  df-rel 5661  df-res 5666

This theorem is referenced by:  resabs1i  5994  resabs1d  5995  resabs2  5996  resiima  6063  fun2ssres  6581  fssres2  6746  smores3  8367  setsres  17197  gsum2dlem2  19952  lindsss  21784  resthauslem  23301  ptcmpfi  23751  tsmsres  24082  ressxms  24464  nrginvrcn  24631  xrge0gsumle  24773  lebnumii  24916  dvmptresicc  25869  dfrelog  26526  relogf1o  26527  dvlog  26612  dvlog2  26614  efopnlem2  26618  wilthlem2  27031  nosupres  27671  nosupbnd2lem1  27679  noinfres  27686  noinfbnd2lem1  27694  nosupinfsep  27696  gsumle  33092  rrhre  34052  iwrdsplit  34419  rpsqrtcn  34625  pthhashvtx  35150  cvmsss2  35296  mbfposadd  37691  mzpcompact2lem  42774  eldioph2  42785  diophin  42795  diophrex  42798  2rexfrabdioph  42819  3rexfrabdioph  42820  4rexfrabdioph  42821  6rexfrabdioph  42822  7rexfrabdioph  42823  fourierdlem46  46181  fourierdlem57  46192  fourierdlem111  46246  fouriersw  46260  psmeasurelem  46499