Theorem resabs1 5997

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-rel 5658  df-res 5663

This theorem is used by:  resabs1i  5998  resabs1d  5999  resabs2  6000  resiima  6074  fun2ssres  6583  fssres2  6748  smores3  8354  setsres  17349  gsum2dlem2  20178  gsumle  20352  lindsss  22123  resthauslem  23674  ptcmpfi  24125  tsmsres  24456  ressxms  24837  nrginvrcn  25004  xrge0gsumle  25146  lebnumii  25280  dvmptresicc  26229  dfrelog  26886  relogf1o  26887  dvlog  26972  dvlog2  26974  efopnlem2  26978  wilthlem2  27389  nosupres  28057  nosupbnd2lem1  28065  noinfres  28072  noinfbnd2lem1  28080  nosupinfsep  28082  pthhashvtx  30308  rrhre  34646  iwrdsplit  35012  rpsqrtcn  35215  cvmsss2  36018  mbfposadd  38565  mzpcompact2lem  43741  eldioph2  43752  diophin  43762  diophrex  43765  2rexfrabdioph  43782  3rexfrabdioph  43783  4rexfrabdioph  43784  6rexfrabdioph  43785  7rexfrabdioph  43786  fourierdlem46  47131  fourierdlem57  47142  fourierdlem111  47196  fouriersw  47210  psmeasurelem  47449