Theorem resabs1 5910

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 5893	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4146	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5875	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 216	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2790	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3882   ⊆ wss 3883   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586  df-rel 5587  df-res 5592

This theorem is referenced by:  resabs1d  5911  resabs2  5912  resiima  5973  fun2ssres  6463  fssres2  6626  smores3  8155  setsres  16807  gsum2dlem2  19487  lindsss  20941  resthauslem  22422  ptcmpfi  22872  tsmsres  23203  ressxms  23587  nrginvrcn  23762  xrge0gsumle  23902  lebnumii  24035  dvmptresicc  24985  dfrelog  25626  relogf1o  25627  dvlog  25711  dvlog2  25713  efopnlem2  25717  wilthlem2  26123  gsumle  31252  rrhre  31871  iwrdsplit  32254  rpsqrtcn  32473  pthhashvtx  32989  cvmsss2  33136  nosupres  33837  nosupbnd2lem1  33845  noinfres  33852  noinfbnd2lem1  33860  nosupinfsep  33862  mbfposadd  35751  mzpcompact2lem  40489  eldioph2  40500  diophin  40510  diophrex  40513  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  resabs1i  42583  fourierdlem46  43583  fourierdlem57  43594  fourierdlem111  43648  fouriersw  43662  psmeasurelem  43898