Theorem resabs1d 6028

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211  df-xp 5695  df-rel 5696  df-res 5701

This theorem is referenced by:  f2ndf  8144  frrlem12  8321  ablfac1eulem  20107  funcrngcsetc  20657  funcrngcsetcALT  20658  funcringcsetc  20691  kgencn2  23581  tsmsres  24168  resubmet  24838  xrge0gsumle  24869  cmssmscld  25398  cmsss  25399  cmscsscms  25421  minveclem3a  25475  dvmptresicc  25966  dvlip2  26049  c1liplem1  26050  efcvx  26508  logccv  26720  loglesqrt  26819  wilthlem2  27127  nosupno  27763  nosupbnd1lem1  27768  nosupbnd2  27776  noinfno  27778  noinfbnd1lem1  27783  noinfbnd2  27791  symgcom2  33087  cyc3conja  33160  bnj1280  35013  cvmlift2lem9  35296  mbfresfi  37653  ssbnd  37775  prdsbnd2  37782  cnpwstotbnd  37784  reheibor  37826  diophin  42760  fnwe2lem2  43040  dvsid  44327  limcresiooub  45598  limcresioolb  45599  fourierdlem46  46108  fourierdlem48  46110  fourierdlem49  46111  fourierdlem58  46120  fourierdlem72  46134  fourierdlem73  46135  fourierdlem74  46136  fourierdlem75  46137  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem93  46155  fourierdlem100  46162  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem107  46169  fourierdlem111  46173  fourierdlem112  46174  fourierdlem114  46176  afvres  47122  afv2res  47189