Theorem resabs1 6012

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900   ∩ cin 4092   ↾ cres 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5172  df-xp 5662  df-rel 5663  df-res 5668

This theorem is used by:  resabs1i  6013  resabs1d  6014  resabs2  6015  resiima  6090  fun2ssres  6611  fssres2  6778  smores3  8397  setsres  17397  gsum2dlem2  20227  gsumle  20401  lindsss  22174  resthauslem  23725  ptcmpfi  24176  tsmsres  24507  ressxms  24888  nrginvrcn  25055  xrge0gsumle  25197  lebnumii  25331  dvmptresicc  26280  dfrelog  26939  relogf1o  26940  dvlog  27025  dvlog2  27027  efopnlem2  27031  wilthlem2  27442  nosupres  28110  nosupbnd2lem1  28118  noinfres  28125  noinfbnd2lem1  28133  nosupinfsep  28135  pthhashvtx  30361  rrhre  34757  iwrdsplit  35123  rpsqrtcn  35326  cvmsss2  36240  mbfposadd  38846  mzpcompact2lem  44022  eldioph2  44033  diophin  44043  diophrex  44046  2rexfrabdioph  44063  3rexfrabdioph  44064  4rexfrabdioph  44065  6rexfrabdioph  44066  7rexfrabdioph  44067  fourierdlem46  47429  fourierdlem57  47440  fourierdlem111  47494  fouriersw  47508  psmeasurelem  47747