Theorem resabs1d 5911

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 5910	. 2 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586  df-rel 5587  df-res 5592

This theorem is referenced by:  f2ndf  7932  frrlem12  8084  ablfac1eulem  19590  kgencn2  22616  tsmsres  23203  resubmet  23871  xrge0gsumle  23902  cmssmscld  24419  cmsss  24420  cmscsscms  24442  minveclem3a  24496  dvmptresicc  24985  dvlip2  25064  c1liplem1  25065  efcvx  25513  logccv  25723  loglesqrt  25816  wilthlem2  26123  symgcom2  31255  cyc3conja  31326  bnj1280  32900  cvmlift2lem9  33173  nosupno  33833  nosupbnd1lem1  33838  nosupbnd2  33846  noinfno  33848  noinfbnd1lem1  33853  noinfbnd2  33861  mbfresfi  35750  ssbnd  35873  prdsbnd2  35880  cnpwstotbnd  35882  reheibor  35924  diophin  40510  fnwe2lem2  40792  dvsid  41838  limcresiooub  43073  limcresioolb  43074  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem58  43595  fourierdlem72  43609  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem93  43630  fourierdlem100  43637  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierdlem112  43649  fourierdlem114  43651  afvres  44551  afv2res  44618  funcrngcsetc  45444  funcrngcsetcALT  45445  funcringcsetc  45481