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

Theorem resabs1 5972
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 5955 . 2 ((𝐴𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶𝐵))
2 sseqin2 4180 . . 3 (𝐵𝐶 ↔ (𝐶𝐵) = 𝐵)
3 reseq2 5937 . . 3 ((𝐶𝐵) = 𝐵 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
42, 3sylbi 216 . 2 (𝐵𝐶 → (𝐴 ↾ (𝐶𝐵)) = (𝐴𝐵))
51, 4eqtrid 2789 1 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cin 3914  wss 3915  cres 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644  df-rel 5645  df-res 5650
This theorem is referenced by:  resabs1d  5973  resabs2  5974  resiima  6033  fun2ssres  6551  fssres2  6715  smores3  8304  setsres  17057  gsum2dlem2  19755  lindsss  21246  resthauslem  22730  ptcmpfi  23180  tsmsres  23511  ressxms  23897  nrginvrcn  24072  xrge0gsumle  24212  lebnumii  24345  dvmptresicc  25296  dfrelog  25937  relogf1o  25938  dvlog  26022  dvlog2  26024  efopnlem2  26028  wilthlem2  26434  nosupres  27071  nosupbnd2lem1  27079  noinfres  27086  noinfbnd2lem1  27094  nosupinfsep  27096  gsumle  31974  rrhre  32642  iwrdsplit  33027  rpsqrtcn  33246  pthhashvtx  33761  cvmsss2  33908  mbfposadd  36154  mzpcompact2lem  41103  eldioph2  41114  diophin  41124  diophrex  41127  2rexfrabdioph  41148  3rexfrabdioph  41149  4rexfrabdioph  41150  6rexfrabdioph  41151  7rexfrabdioph  41152  resabs1i  43429  fourierdlem46  44467  fourierdlem57  44478  fourierdlem111  44532  fouriersw  44546  psmeasurelem  44785
  Copyright terms: Public domain W3C validator