Theorem resabs1 5973

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

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

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  resabs1i  5974  resabs1d  5975  resabs2  5976  resiima  6043  fun2ssres  6545  fssres2  6710  smores3  8295  setsres  17117  gsum2dlem2  19912  gsumle  20086  lindsss  21791  resthauslem  23319  ptcmpfi  23769  tsmsres  24100  ressxms  24481  nrginvrcn  24648  xrge0gsumle  24790  lebnumii  24933  dvmptresicc  25885  dfrelog  26542  relogf1o  26543  dvlog  26628  dvlog2  26630  efopnlem2  26634  wilthlem2  27047  nosupres  27687  nosupbnd2lem1  27695  noinfres  27702  noinfbnd2lem1  27710  nosupinfsep  27712  rrhre  34198  iwrdsplit  34564  rpsqrtcn  34770  pthhashvtx  35341  cvmsss2  35487  mbfposadd  37915  mzpcompact2lem  43105  eldioph2  43116  diophin  43126  diophrex  43129  2rexfrabdioph  43150  3rexfrabdioph  43151  4rexfrabdioph  43152  6rexfrabdioph  43153  7rexfrabdioph  43154  fourierdlem46  46507  fourierdlem57  46518  fourierdlem111  46572  fouriersw  46586  psmeasurelem  46825