Theorem resabs1d 5995

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660  df-rel 5661  df-res 5666

This theorem is referenced by:  f2ndf  8119  frrlem12  8296  ablfac1eulem  20055  funcrngcsetc  20600  funcrngcsetcALT  20601  funcringcsetc  20634  kgencn2  23495  tsmsres  24082  resubmet  24741  xrge0gsumle  24773  cmssmscld  25302  cmsss  25303  cmscsscms  25325  minveclem3a  25379  dvmptresicc  25869  dvlip2  25952  c1liplem1  25953  efcvx  26411  logccv  26624  loglesqrt  26723  wilthlem2  27031  nosupno  27667  nosupbnd1lem1  27672  nosupbnd2  27680  noinfno  27682  noinfbnd1lem1  27687  noinfbnd2  27695  symgcom2  33095  cyc3conja  33168  bnj1280  35051  cvmlift2lem9  35333  mbfresfi  37690  ssbnd  37812  prdsbnd2  37819  cnpwstotbnd  37821  reheibor  37863  diophin  42795  fnwe2lem2  43075  dvsid  44355  limcresiooub  45671  limcresioolb  45672  fourierdlem46  46181  fourierdlem48  46183  fourierdlem49  46184  fourierdlem58  46193  fourierdlem72  46207  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem89  46224  fourierdlem90  46225  fourierdlem91  46226  fourierdlem93  46228  fourierdlem100  46235  fourierdlem102  46237  fourierdlem103  46238  fourierdlem104  46239  fourierdlem107  46242  fourierdlem111  46246  fourierdlem112  46247  fourierdlem114  46249  afvres  47201  afv2res  47268