Theorem resabs1 5966

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 5952	. 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵))
2		sseqin2 4182	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵)
3		reseq2 5934	. . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
4	2, 3	sylbi 217	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵))
5	1, 4	eqtrid 2776	1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3910   ⊆ wss 3911   ↾ cres 5633

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  resabs1i  5967  resabs1d  5968  resabs2  5969  resiima  6036  fun2ssres  6545  fssres2  6710  smores3  8299  setsres  17124  gsum2dlem2  19877  lindsss  21709  resthauslem  23226  ptcmpfi  23676  tsmsres  24007  ressxms  24389  nrginvrcn  24556  xrge0gsumle  24698  lebnumii  24841  dvmptresicc  25793  dfrelog  26450  relogf1o  26451  dvlog  26536  dvlog2  26538  efopnlem2  26542  wilthlem2  26955  nosupres  27595  nosupbnd2lem1  27603  noinfres  27610  noinfbnd2lem1  27618  nosupinfsep  27620  gsumle  33011  rrhre  33984  iwrdsplit  34351  rpsqrtcn  34557  pthhashvtx  35088  cvmsss2  35234  mbfposadd  37634  mzpcompact2lem  42712  eldioph2  42723  diophin  42733  diophrex  42736  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  fourierdlem46  46123  fourierdlem57  46134  fourierdlem111  46188  fouriersw  46202  psmeasurelem  46441