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

Theorem resabs1d 5973
Description: Absorption law for restriction, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
resabs1d.b (𝜑𝐵𝐶)
Assertion
Ref Expression
resabs1d (𝜑 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))

Proof of Theorem resabs1d
StepHypRef Expression
1 resabs1d.b . 2 (𝜑𝐵𝐶)
2 resabs1 5972 . 2 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
31, 2syl 17 1 (𝜑 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  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:  f2ndf  8057  frrlem12  8233  ablfac1eulem  19858  kgencn2  22924  tsmsres  23511  resubmet  24181  xrge0gsumle  24212  cmssmscld  24730  cmsss  24731  cmscsscms  24753  minveclem3a  24807  dvmptresicc  25296  dvlip2  25375  c1liplem1  25376  efcvx  25824  logccv  26034  loglesqrt  26127  wilthlem2  26434  nosupno  27067  nosupbnd1lem1  27072  nosupbnd2  27080  noinfno  27082  noinfbnd1lem1  27087  noinfbnd2  27095  symgcom2  31977  cyc3conja  32048  bnj1280  33672  cvmlift2lem9  33945  mbfresfi  36153  ssbnd  36276  prdsbnd2  36283  cnpwstotbnd  36285  reheibor  36327  diophin  41124  fnwe2lem2  41407  dvsid  42685  limcresiooub  43957  limcresioolb  43958  fourierdlem46  44467  fourierdlem48  44469  fourierdlem49  44470  fourierdlem58  44479  fourierdlem72  44493  fourierdlem73  44494  fourierdlem74  44495  fourierdlem75  44496  fourierdlem89  44510  fourierdlem90  44511  fourierdlem91  44512  fourierdlem93  44514  fourierdlem100  44521  fourierdlem102  44523  fourierdlem103  44524  fourierdlem104  44525  fourierdlem107  44528  fourierdlem111  44532  fourierdlem112  44533  fourierdlem114  44535  afvres  45478  afv2res  45545  funcrngcsetc  46370  funcrngcsetcALT  46371  funcringcsetc  46407
  Copyright terms: Public domain W3C validator