Theorem resabs1 5722

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 5705	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4074	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5683	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 209	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	syl5eq 2820	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1507   ∩ cin 3824   ⊆ wss 3825   ↾ cres 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-opab 4986  df-xp 5406  df-rel 5407  df-res 5412

This theorem is referenced by:  resabs1d  5723  resabs2  5724  resiima  5778  fun2ssres  6226  fssres2  6369  smores3  7787  setsres  16371  gsum2dlem2  18834  lindsss  20660  resthauslem  21665  ptcmpfi  22115  tsmsres  22445  ressxms  22828  nrginvrcn  22994  xrge0gsumle  23134  lebnumii  23263  dfrelog  24840  relogf1o  24841  dvlog  24925  dvlog2  24927  efopnlem2  24931  wilthlem2  25338  gsumle  30478  rrhre  30863  iwrdsplit  31247  iwrdsplitOLD  31248  rpsqrtcn  31473  cvmsss2  32066  nosupres  32668  nosupbnd2lem1  32676  mbfposadd  34328  mzpcompact2lem  38688  eldioph2  38699  diophin  38710  diophrex  38713  2rexfrabdioph  38734  3rexfrabdioph  38735  4rexfrabdioph  38736  6rexfrabdioph  38737  7rexfrabdioph  38738  resabs1i  40782  dvmptresicc  41580  fourierdlem46  41814  fourierdlem57  41825  fourierdlem111  41879  fouriersw  41893  psmeasurelem  42129