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

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3913   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  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  19865  kgencn2  22945  tsmsres  23532  resubmet  24202  xrge0gsumle  24233  cmssmscld  24751  cmsss  24752  cmscsscms  24774  minveclem3a  24828  dvmptresicc  25317  dvlip2  25396  c1liplem1  25397  efcvx  25845  logccv  26055  loglesqrt  26148  wilthlem2  26455  nosupno  27088  nosupbnd1lem1  27093  nosupbnd2  27101  noinfno  27103  noinfbnd1lem1  27108  noinfbnd2  27116  symgcom2  32005  cyc3conja  32076  bnj1280  33721  cvmlift2lem9  33992  mbfresfi  36197  ssbnd  36320  prdsbnd2  36327  cnpwstotbnd  36329  reheibor  36371  diophin  41153  fnwe2lem2  41436  dvsid  42733  limcresiooub  44003  limcresioolb  44004  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem58  44525  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  fourierdlem93  44560  fourierdlem100  44567  fourierdlem102  44569  fourierdlem103  44570  fourierdlem104  44571  fourierdlem107  44574  fourierdlem111  44578  fourierdlem112  44579  fourierdlem114  44581  afvres  45524  afv2res  45591  funcrngcsetc  46416  funcrngcsetcALT  46417  funcringcsetc  46453