Theorem resabs1 6010

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 5993	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4214	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5975	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 216	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2782	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3946   ⊆ wss 3947   ↾ cres 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-xp 5681  df-rel 5682  df-res 5687

This theorem is referenced by:  resabs1d  6011  resabs2  6012  resiima  6074  fun2ssres  6592  fssres2  6758  smores3  8355  setsres  17115  gsum2dlem2  19880  lindsss  21598  resthauslem  23087  ptcmpfi  23537  tsmsres  23868  ressxms  24254  nrginvrcn  24429  xrge0gsumle  24569  lebnumii  24712  dvmptresicc  25665  dfrelog  26310  relogf1o  26311  dvlog  26395  dvlog2  26397  efopnlem2  26401  wilthlem2  26809  nosupres  27446  nosupbnd2lem1  27454  noinfres  27461  noinfbnd2lem1  27469  nosupinfsep  27471  gsumle  32512  rrhre  33299  iwrdsplit  33684  rpsqrtcn  33903  pthhashvtx  34416  cvmsss2  34563  mbfposadd  36838  mzpcompact2lem  41791  eldioph2  41802  diophin  41812  diophrex  41815  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  resabs1i  44135  fourierdlem46  45166  fourierdlem57  45177  fourierdlem111  45231  fouriersw  45245  psmeasurelem  45484