Theorem resabs1 6007

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 4177	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5975	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 220	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2810	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1570   ∩ cin 3905   ⊆ wss 3906   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-xp 5669  df-rel 5670  df-res 5675

This theorem is referenced by:  resabs1i  6008  resabs1d  6009  resabs2  6010  resiima  6080  fun2ssres  6583  fssres2  6748  smores3  8341  setsres  17239  gsum2dlem2  20042  gsumle  20216  lindsss  21955  resthauslem  23501  ptcmpfi  23951  tsmsres  24282  ressxms  24663  nrginvrcn  24830  xrge0gsumle  24972  lebnumii  25106  dvmptresicc  26056  dfrelog  26711  relogf1o  26712  dvlog  26797  dvlog2  26799  efopnlem2  26803  wilthlem2  27214  nosupres  27852  nosupbnd2lem1  27860  noinfres  27867  noinfbnd2lem1  27875  nosupinfsep  27877  rrhre  34392  iwrdsplit  34758  rpsqrtcn  34961  pthhashvtx  35601  cvmsss2  35747  mbfposadd  38299  mzpcompact2lem  43465  eldioph2  43476  diophin  43486  diophrex  43489  2rexfrabdioph  43506  3rexfrabdioph  43507  4rexfrabdioph  43508  6rexfrabdioph  43509  7rexfrabdioph  43510  fourierdlem46  46849  fourierdlem57  46860  fourierdlem111  46914  fouriersw  46928  psmeasurelem  47167