Theorem resabs1 5999

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 3898   ⊆ wss 3899   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5661  df-rel 5662  df-res 5667

This theorem is used by:  resabs1i  6000  resabs1d  6001  resabs2  6002  resiima  6072  fun2ssres  6578  fssres2  6743  smores3  8342  setsres  17270  gsum2dlem2  20098  gsumle  20272  lindsss  22037  resthauslem  23588  ptcmpfi  24039  tsmsres  24370  ressxms  24751  nrginvrcn  24918  xrge0gsumle  25060  lebnumii  25194  dvmptresicc  26143  dfrelog  26802  relogf1o  26803  dvlog  26888  dvlog2  26890  efopnlem2  26894  wilthlem2  27305  nosupres  27943  nosupbnd2lem1  27951  noinfres  27958  noinfbnd2lem1  27966  nosupinfsep  27968  pthhashvtx  30194  rrhre  34531  iwrdsplit  34898  rpsqrtcn  35101  cvmsss2  35853  mbfposadd  38416  mzpcompact2lem  43596  eldioph2  43607  diophin  43617  diophrex  43620  2rexfrabdioph  43637  3rexfrabdioph  43638  4rexfrabdioph  43639  6rexfrabdioph  43640  7rexfrabdioph  43641  fourierdlem46  46980  fourierdlem57  46991  fourierdlem111  47045  fouriersw  47059  psmeasurelem  47298