Theorem resabs1d 6026

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951   ↾ cres 5687

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691  df-rel 5692  df-res 5697

This theorem is referenced by:  f2ndf  8145  frrlem12  8322  ablfac1eulem  20092  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  kgencn2  23565  tsmsres  24152  resubmet  24823  xrge0gsumle  24855  cmssmscld  25384  cmsss  25385  cmscsscms  25407  minveclem3a  25461  dvmptresicc  25951  dvlip2  26034  c1liplem1  26035  efcvx  26493  logccv  26705  loglesqrt  26804  wilthlem2  27112  nosupno  27748  nosupbnd1lem1  27753  nosupbnd2  27761  noinfno  27763  noinfbnd1lem1  27768  noinfbnd2  27776  symgcom2  33104  cyc3conja  33177  bnj1280  35034  cvmlift2lem9  35316  mbfresfi  37673  ssbnd  37795  prdsbnd2  37802  cnpwstotbnd  37804  reheibor  37846  diophin  42783  fnwe2lem2  43063  dvsid  44350  limcresiooub  45657  limcresioolb  45658  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem58  46179  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem93  46214  fourierdlem100  46221  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierdlem112  46233  fourierdlem114  46235  afvres  47184  afv2res  47251