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

Theorem resabs1 5965
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 5948 . 2 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
2 sseqin2 4173 . . 3 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
3 reseq2 5930 . . 3 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
42, 3sylbi 216 . 2 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
51, 4eqtrid 2788 1 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cin 3907  wss 3908  cres 5633
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5166  df-xp 5637  df-rel 5638  df-res 5643
This theorem is referenced by:  resabs1d  5966  resabs2  5967  resiima  6026  fun2ssres  6543  fssres2  6707  smores3  8291  setsres  17004  gsum2dlem2  19701  lindsss  21177  resthauslem  22660  ptcmpfi  23110  tsmsres  23441  ressxms  23827  nrginvrcn  24002  xrge0gsumle  24142  lebnumii  24275  dvmptresicc  25226  dfrelog  25867  relogf1o  25868  dvlog  25952  dvlog2  25954  efopnlem2  25958  wilthlem2  26364  nosupres  27001  nosupbnd2lem1  27009  noinfres  27016  noinfbnd2lem1  27024  nosupinfsep  27026  gsumle  31774  rrhre  32430  iwrdsplit  32815  rpsqrtcn  33034  pthhashvtx  33549  cvmsss2  33696  mbfposadd  36057  mzpcompact2lem  40977  eldioph2  40988  diophin  40998  diophrex  41001  2rexfrabdioph  41022  3rexfrabdioph  41023  4rexfrabdioph  41024  6rexfrabdioph  41025  7rexfrabdioph  41026  resabs1i  43260  fourierdlem46  44288  fourierdlem57  44299  fourierdlem111  44353  fouriersw  44367  psmeasurelem  44606
  Copyright terms: Public domain W3C validator