Theorem resabs1d 6009

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-xp 5669  df-rel 5670  df-res 5675

This theorem is referenced by:  f2ndf  8116  frrlem12  8295  ablfac1eulem  20145  funcrngcsetc  20726  funcrngcsetcALT  20727  funcringcsetc  20760  kgencn2  23695  tsmsres  24282  resubmet  24940  xrge0gsumle  24972  cmssmscld  25490  cmsss  25491  cmscsscms  25513  minveclem3a  25567  dvmptresicc  26056  dvlip2  26135  c1liplem1  26136  efcvx  26590  logccv  26806  loglesqrt  26904  wilthlem2  27211  nosupno  27845  nosupbnd1lem1  27850  nosupbnd2  27858  noinfno  27860  noinfbnd1lem1  27865  noinfbnd2  27873  symgcom2  33382  cyc3conja  33455  bnj1280  35386  cvmlift2lem9  35781  mbfresfi  38295  ssbnd  38417  prdsbnd2  38424  cnpwstotbnd  38426  reheibor  38468  diophin  43483  fnwe2lem2  43758  dvsid  45021  limcresiooub  46336  limcresioolb  46337  fourierdlem46  46846  fourierdlem48  46848  fourierdlem49  46849  fourierdlem58  46858  fourierdlem72  46872  fourierdlem73  46873  fourierdlem74  46874  fourierdlem75  46875  fourierdlem89  46889  fourierdlem90  46890  fourierdlem91  46891  fourierdlem93  46893  fourierdlem100  46900  fourierdlem102  46902  fourierdlem103  46903  fourierdlem104  46904  fourierdlem107  46907  fourierdlem111  46911  fourierdlem112  46912  fourierdlem114  46914  afvres  47886  afv2res  47953