Theorem resabs1d 5961

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  f2ndf  8056  frrlem12  8233  ablfac1eulem  19988  funcrngcsetc  20557  funcrngcsetcALT  20558  funcringcsetc  20591  kgencn2  23473  tsmsres  24060  resubmet  24718  xrge0gsumle  24750  cmssmscld  25278  cmsss  25279  cmscsscms  25301  minveclem3a  25355  dvmptresicc  25845  dvlip2  25928  c1liplem1  25929  efcvx  26387  logccv  26600  loglesqrt  26699  wilthlem2  27007  nosupno  27643  nosupbnd1lem1  27648  nosupbnd2  27656  noinfno  27658  noinfbnd1lem1  27663  noinfbnd2  27671  symgcom2  33060  cyc3conja  33133  bnj1280  35053  cvmlift2lem9  35376  mbfresfi  37727  ssbnd  37849  prdsbnd2  37856  cnpwstotbnd  37858  reheibor  37900  diophin  42890  fnwe2lem2  43169  dvsid  44449  limcresiooub  45765  limcresioolb  45766  fourierdlem46  46275  fourierdlem48  46277  fourierdlem49  46278  fourierdlem58  46287  fourierdlem72  46301  fourierdlem73  46302  fourierdlem74  46303  fourierdlem75  46304  fourierdlem89  46318  fourierdlem90  46319  fourierdlem91  46320  fourierdlem93  46322  fourierdlem100  46329  fourierdlem102  46331  fourierdlem103  46332  fourierdlem104  46333  fourierdlem107  46336  fourierdlem111  46340  fourierdlem112  46341  fourierdlem114  46343  afvres  47297  afv2res  47364