MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resabs1 Structured version   Visualization version   GIF version

Theorem resabs1 5870
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
StepHypRef Expression
1 resres 5853 . 2 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
2 sseqin2 4177 . . 3 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
3 reseq2 5835 . . 3 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
42, 3sylbi 220 . 2 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
51, 4syl5eq 2871 1 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cin 3918  wss 3919  cres 5544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3142  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-opab 5115  df-xp 5548  df-rel 5549  df-res 5554
This theorem is referenced by:  resabs1d  5871  resabs2  5872  resiima  5931  fun2ssres  6387  fssres2  6536  smores3  7986  setsres  16525  gsum2dlem2  19091  lindsss  20520  resthauslem  21975  ptcmpfi  22425  tsmsres  22756  ressxms  23139  nrginvrcn  23305  xrge0gsumle  23445  lebnumii  23578  dvmptresicc  24526  dfrelog  25164  relogf1o  25165  dvlog  25249  dvlog2  25251  efopnlem2  25255  wilthlem2  25661  gsumle  30761  rrhre  31323  iwrdsplit  31706  rpsqrtcn  31925  pthhashvtx  32435  cvmsss2  32582  nosupres  33268  nosupbnd2lem1  33276  mbfposadd  35053  mzpcompact2lem  39613  eldioph2  39624  diophin  39634  diophrex  39637  2rexfrabdioph  39658  3rexfrabdioph  39659  4rexfrabdioph  39660  6rexfrabdioph  39661  7rexfrabdioph  39662  resabs1i  41710  fourierdlem46  42725  fourierdlem57  42736  fourierdlem111  42790  fouriersw  42804  psmeasurelem  43040
  Copyright terms: Public domain W3C validator