Theorem resabs1d 5967

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-opab 5142  df-xp 5631  df-rel 5632  df-res 5637

This theorem is referenced by:  f2ndf  8066  frrlem12  8244  ablfac1eulem  20047  funcrngcsetc  20619  funcrngcsetcALT  20620  funcringcsetc  20653  kgencn2  23547  tsmsres  24134  resubmet  24792  xrge0gsumle  24824  cmssmscld  25342  cmsss  25343  cmscsscms  25365  minveclem3a  25419  dvmptresicc  25908  dvlip2  25987  c1liplem1  25988  efcvx  26439  logccv  26652  loglesqrt  26750  wilthlem2  27057  nosupno  27692  nosupbnd1lem1  27697  nosupbnd2  27705  noinfno  27707  noinfbnd1lem1  27712  noinfbnd2  27720  symgcom2  33172  cyc3conja  33245  bnj1280  35209  cvmlift2lem9  35546  mbfresfi  38040  ssbnd  38162  prdsbnd2  38169  cnpwstotbnd  38171  reheibor  38213  diophin  43228  fnwe2lem2  43503  dvsid  44782  limcresiooub  46092  limcresioolb  46093  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem58  46614  fourierdlem72  46628  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem93  46649  fourierdlem100  46656  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  fourierdlem111  46667  fourierdlem112  46668  fourierdlem114  46670  afvres  47642  afv2res  47709