Theorem resabs1 5958

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 5944	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4152	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5926	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 218	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2786	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-opab 5135  df-xp 5624  df-rel 5625  df-res 5630

This theorem is referenced by:  resabs1i  5959  resabs1d  5960  resabs2  5961  resiima  6028  fun2ssres  6530  fssres2  6695  smores3  8283  setsres  17139  gsum2dlem2  19937  gsumle  20111  lindsss  21799  resthauslem  23346  ptcmpfi  23796  tsmsres  24127  ressxms  24508  nrginvrcn  24675  xrge0gsumle  24817  lebnumii  24951  dvmptresicc  25901  dfrelog  26547  relogf1o  26548  dvlog  26633  dvlog2  26635  efopnlem2  26639  wilthlem2  27050  nosupres  27689  nosupbnd2lem1  27697  noinfres  27704  noinfbnd2lem1  27712  nosupinfsep  27714  rrhre  34205  iwrdsplit  34571  rpsqrtcn  34777  pthhashvtx  35356  cvmsss2  35502  mbfposadd  38034  mzpcompact2lem  43200  eldioph2  43211  diophin  43221  diophrex  43224  2rexfrabdioph  43241  3rexfrabdioph  43242  4rexfrabdioph  43243  6rexfrabdioph  43244  7rexfrabdioph  43245  fourierdlem46  46595  fourierdlem57  46606  fourierdlem111  46660  fouriersw  46674  psmeasurelem  46913