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

Theorem resabs1d 5426
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 5425 . 2 (𝐵𝐶 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
31, 2syl 17 1 (𝜑 → ((𝐴𝐶) ↾ 𝐵) = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  wss 3572  cres 5114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-opab 4711  df-xp 5118  df-rel 5119  df-res 5124
This theorem is referenced by:  f2ndf  7280  ablfac1eulem  18465  kgencn2  21354  tsmsres  21941  resubmet  22599  xrge0gsumle  22630  cmsss  23141  minveclem3a  23192  dvlip2  23752  c1liplem1  23753  efcvx  24197  logccv  24403  loglesqrt  24493  wilthlem2  24789  bnj1280  31073  cvmlift2lem9  31278  nosupno  31833  nosupbnd1lem1  31838  nosupbnd2  31846  mbfresfi  33436  ssbnd  33567  prdsbnd2  33574  cnpwstotbnd  33576  reheibor  33618  diophin  37162  fnwe2lem2  37447  dvsid  38356  limcresiooub  39680  limcresioolb  39681  dvmptresicc  39903  fourierdlem46  40138  fourierdlem48  40140  fourierdlem49  40141  fourierdlem58  40150  fourierdlem72  40164  fourierdlem73  40165  fourierdlem74  40166  fourierdlem75  40167  fourierdlem89  40181  fourierdlem90  40182  fourierdlem91  40183  fourierdlem93  40185  fourierdlem100  40192  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem107  40199  fourierdlem111  40203  fourierdlem112  40204  fourierdlem114  40206  afvres  41021  funcrngcsetc  41769  funcrngcsetcALT  41770  funcringcsetc  41806
  Copyright terms: Public domain W3C validator