Theorem resabs1d 5998

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5168  df-xp 5658  df-rel 5659  df-res 5664

This theorem is referenced by:  f2ndf  8103  frrlem12  8282  ablfac1eulem  20135  funcrngcsetc  20716  funcrngcsetcALT  20717  funcringcsetc  20750  kgencn2  23675  tsmsres  24262  resubmet  24920  xrge0gsumle  24952  cmssmscld  25470  cmsss  25471  cmscsscms  25493  minveclem3a  25547  dvmptresicc  26036  dvlip2  26115  c1liplem1  26116  efcvx  26570  logccv  26786  loglesqrt  26884  wilthlem2  27191  nosupno  27825  nosupbnd1lem1  27830  nosupbnd2  27838  noinfno  27840  noinfbnd1lem1  27845  noinfbnd2  27853  symgcom2  33317  cyc3conja  33390  bnj1280  35325  cvmlift2lem9  35674  mbfresfi  38177  ssbnd  38299  prdsbnd2  38306  cnpwstotbnd  38308  reheibor  38350  diophin  43365  fnwe2lem2  43640  dvsid  44905  limcresiooub  46214  limcresioolb  46215  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem58  46736  fourierdlem72  46750  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem93  46771  fourierdlem100  46778  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem107  46785  fourierdlem111  46789  fourierdlem112  46790  fourierdlem114  46792  afvres  47764  afv2res  47831