Theorem resabs1 5965

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3889   ⊆ wss 3890   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  resabs1i  5966  resabs1d  5967  resabs2  5968  resiima  6035  fun2ssres  6537  fssres2  6702  smores3  8286  setsres  17139  gsum2dlem2  19937  gsumle  20111  lindsss  21814  resthauslem  23338  ptcmpfi  23788  tsmsres  24119  ressxms  24500  nrginvrcn  24667  xrge0gsumle  24809  lebnumii  24943  dvmptresicc  25893  dfrelog  26542  relogf1o  26543  dvlog  26628  dvlog2  26630  efopnlem2  26634  wilthlem2  27046  nosupres  27685  nosupbnd2lem1  27693  noinfres  27700  noinfbnd2lem1  27708  nosupinfsep  27710  rrhre  34181  iwrdsplit  34547  rpsqrtcn  34753  pthhashvtx  35326  cvmsss2  35472  mbfposadd  38002  mzpcompact2lem  43197  eldioph2  43208  diophin  43218  diophrex  43221  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  fourierdlem46  46598  fourierdlem57  46609  fourierdlem111  46663  fouriersw  46677  psmeasurelem  46916