Theorem resabs1d 6037

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

Step	Hyp	Ref	Expression
1		resabs1d.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		resabs1 6036	. 2 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-xp 5706  df-rel 5707  df-res 5712

This theorem is referenced by:  f2ndf  8161  frrlem12  8338  ablfac1eulem  20116  funcrngcsetc  20662  funcrngcsetcALT  20663  funcringcsetc  20696  kgencn2  23586  tsmsres  24173  resubmet  24843  xrge0gsumle  24874  cmssmscld  25403  cmsss  25404  cmscsscms  25426  minveclem3a  25480  dvmptresicc  25971  dvlip2  26054  c1liplem1  26055  efcvx  26511  logccv  26723  loglesqrt  26822  wilthlem2  27130  nosupno  27766  nosupbnd1lem1  27771  nosupbnd2  27779  noinfno  27781  noinfbnd1lem1  27786  noinfbnd2  27794  symgcom2  33077  cyc3conja  33150  bnj1280  34996  cvmlift2lem9  35279  mbfresfi  37626  ssbnd  37748  prdsbnd2  37755  cnpwstotbnd  37757  reheibor  37799  diophin  42728  fnwe2lem2  43008  dvsid  44300  limcresiooub  45563  limcresioolb  45564  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem58  46085  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem100  46127  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierdlem112  46139  fourierdlem114  46141  afvres  47087  afv2res  47154