Theorem resabs1 5957

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3902   ⊆ wss 3903   ↾ cres 5621

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  resabs1i  5958  resabs1d  5959  resabs2  5960  resiima  6027  fun2ssres  6527  fssres2  6692  smores3  8276  setsres  17089  gsum2dlem2  19850  gsumle  20024  lindsss  21731  resthauslem  23248  ptcmpfi  23698  tsmsres  24029  ressxms  24411  nrginvrcn  24578  xrge0gsumle  24720  lebnumii  24863  dvmptresicc  25815  dfrelog  26472  relogf1o  26473  dvlog  26558  dvlog2  26560  efopnlem2  26564  wilthlem2  26977  nosupres  27617  nosupbnd2lem1  27625  noinfres  27632  noinfbnd2lem1  27640  nosupinfsep  27642  rrhre  34004  iwrdsplit  34371  rpsqrtcn  34577  pthhashvtx  35121  cvmsss2  35267  mbfposadd  37667  mzpcompact2lem  42744  eldioph2  42755  diophin  42765  diophrex  42768  2rexfrabdioph  42789  3rexfrabdioph  42790  4rexfrabdioph  42791  6rexfrabdioph  42792  7rexfrabdioph  42793  fourierdlem46  46153  fourierdlem57  46164  fourierdlem111  46218  fouriersw  46232  psmeasurelem  46471