Theorem resabs1d 5849

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526  df-res 5531

This theorem is referenced by:  f2ndf  7799  ablfac1eulem  19187  kgencn2  22162  tsmsres  22749  resubmet  23407  xrge0gsumle  23438  cmssmscld  23954  cmsss  23955  cmscsscms  23977  minveclem3a  24031  dvmptresicc  24519  dvlip2  24598  c1liplem1  24599  efcvx  25044  logccv  25254  loglesqrt  25347  wilthlem2  25654  symgcom2  30778  cyc3conja  30849  bnj1280  32402  cvmlift2lem9  32671  frrlem12  33247  nosupno  33316  nosupbnd1lem1  33321  nosupbnd2  33329  mbfresfi  35103  ssbnd  35226  prdsbnd2  35233  cnpwstotbnd  35235  reheibor  35277  diophin  39713  fnwe2lem2  39995  dvsid  41035  limcresiooub  42284  limcresioolb  42285  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem58  42806  fourierdlem72  42820  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem93  42841  fourierdlem100  42848  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem107  42855  fourierdlem111  42859  fourierdlem112  42860  fourierdlem114  42862  afvres  43728  afv2res  43795  funcrngcsetc  44622  funcrngcsetcALT  44623  funcringcsetc  44659