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

Theorem resabs1d 5862
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 5861 . 2 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
31, 2syl 17 1 (𝜑 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3908  cres 5534
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
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 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-opab 5105  df-xp 5538  df-rel 5539  df-res 5544
This theorem is referenced by:  f2ndf  7803  ablfac1eulem  19185  kgencn2  22160  tsmsres  22747  resubmet  23405  xrge0gsumle  23436  cmssmscld  23952  cmsss  23953  cmscsscms  23975  minveclem3a  24029  dvmptresicc  24517  dvlip2  24596  c1liplem1  24597  efcvx  25042  logccv  25252  loglesqrt  25345  wilthlem2  25652  symgcom2  30759  cyc3conja  30830  bnj1280  32366  cvmlift2lem9  32632  frrlem12  33208  nosupno  33277  nosupbnd1lem1  33282  nosupbnd2  33290  mbfresfi  35062  ssbnd  35185  prdsbnd2  35192  cnpwstotbnd  35194  reheibor  35236  diophin  39644  fnwe2lem2  39926  dvsid  40970  limcresiooub  42224  limcresioolb  42225  fourierdlem46  42734  fourierdlem48  42736  fourierdlem49  42737  fourierdlem58  42746  fourierdlem72  42760  fourierdlem73  42761  fourierdlem74  42762  fourierdlem75  42763  fourierdlem89  42777  fourierdlem90  42778  fourierdlem91  42779  fourierdlem93  42781  fourierdlem100  42788  fourierdlem102  42790  fourierdlem103  42791  fourierdlem104  42792  fourierdlem107  42795  fourierdlem111  42799  fourierdlem112  42800  fourierdlem114  42802  afvres  43668  afv2res  43735  funcrngcsetc  44562  funcrngcsetcALT  44563  funcringcsetc  44599
  Copyright terms: Public domain W3C validator