Theorem resabs1 5996

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 5982	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4120	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5964	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 220	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2807	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895   ∩ cin 4089   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-xp 5656  df-rel 5657  df-res 5662

This theorem is used by:  resabs1i  5997  resabs1d  5998  resabs2  5999  resiima  6073  fun2ssres  6586  fssres2  6751  smores3  8365  setsres  17362  gsum2dlem2  20191  gsumle  20365  lindsss  22136  resthauslem  23687  ptcmpfi  24138  tsmsres  24469  ressxms  24850  nrginvrcn  25017  xrge0gsumle  25159  lebnumii  25293  dvmptresicc  26242  dfrelog  26899  relogf1o  26900  dvlog  26985  dvlog2  26987  efopnlem2  26991  wilthlem2  27402  nosupres  28070  nosupbnd2lem1  28078  noinfres  28085  noinfbnd2lem1  28093  nosupinfsep  28095  pthhashvtx  30321  rrhre  34700  iwrdsplit  35066  rpsqrtcn  35269  cvmsss2  36126  mbfposadd  38679  mzpcompact2lem  43856  eldioph2  43867  diophin  43877  diophrex  43880  2rexfrabdioph  43897  3rexfrabdioph  43898  4rexfrabdioph  43899  6rexfrabdioph  43900  7rexfrabdioph  43901  fourierdlem46  47256  fourierdlem57  47267  fourierdlem111  47321  fouriersw  47335  psmeasurelem  47574