Theorem resabs1d 5999

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5657  df-rel 5658  df-res 5663

This theorem is used by:  f2ndf  8120  frrlem12  8299  ablfac1eulem  20268  funcrngcsetc  20872  funcrngcsetcALT  20873  funcringcsetc  20906  kgencn2  23856  tsmsres  24443  resubmet  25101  xrge0gsumle  25133  cmssmscld  25651  cmsss  25652  cmscsscms  25674  minveclem3a  25728  dvmptresicc  26216  dvlip2  26295  c1liplem1  26296  efcvx  26758  logccv  26973  loglesqrt  27071  wilthlem2  27378  nosupno  28042  nosupbnd1lem1  28047  nosupbnd2  28055  noinfno  28057  noinfbnd1lem1  28062  noinfbnd2  28070  symgcom2  33627  cyc3conja  33700  bnj1280  35633  cvmlift2lem9  36045  mbfresfi  38552  ssbnd  38690  prdsbnd2  38697  cnpwstotbnd  38699  reheibor  38741  diophin  43736  fnwe2lem2  44011  dvsid  45274  limcresiooub  46596  limcresioolb  46597  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem58  47118  fourierdlem72  47132  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem93  47153  fourierdlem100  47160  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem111  47171  fourierdlem112  47172  fourierdlem114  47174  afvres  48186  afv2res  48253