Theorem resabs1d 5963

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-xp 5629  df-rel 5630  df-res 5635

This theorem is referenced by:  f2ndf  8060  frrlem12  8237  ablfac1eulem  19971  funcrngcsetc  20543  funcrngcsetcALT  20544  funcringcsetc  20577  kgencn2  23460  tsmsres  24047  resubmet  24706  xrge0gsumle  24738  cmssmscld  25266  cmsss  25267  cmscsscms  25289  minveclem3a  25343  dvmptresicc  25833  dvlip2  25916  c1liplem1  25917  efcvx  26375  logccv  26588  loglesqrt  26687  wilthlem2  26995  nosupno  27631  nosupbnd1lem1  27636  nosupbnd2  27644  noinfno  27646  noinfbnd1lem1  27651  noinfbnd2  27659  symgcom2  33039  cyc3conja  33112  bnj1280  34986  cvmlift2lem9  35283  mbfresfi  37645  ssbnd  37767  prdsbnd2  37774  cnpwstotbnd  37776  reheibor  37818  diophin  42745  fnwe2lem2  43024  dvsid  44304  limcresiooub  45624  limcresioolb  45625  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem58  46146  fourierdlem72  46160  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem93  46181  fourierdlem100  46188  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem107  46195  fourierdlem111  46199  fourierdlem112  46200  fourierdlem114  46202  afvres  47157  afv2res  47224