Theorem resabs1d 5973

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  f2ndf  8070  frrlem12  8247  ablfac1eulem  20049  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  kgencn2  23522  tsmsres  24109  resubmet  24767  xrge0gsumle  24799  cmssmscld  25317  cmsss  25318  cmscsscms  25340  minveclem3a  25394  dvmptresicc  25883  dvlip2  25962  c1liplem1  25963  efcvx  26414  logccv  26627  loglesqrt  26725  wilthlem2  27032  nosupno  27667  nosupbnd1lem1  27672  nosupbnd2  27680  noinfno  27682  noinfbnd1lem1  27687  noinfbnd2  27695  symgcom2  33145  cyc3conja  33218  bnj1280  35162  cvmlift2lem9  35493  mbfresfi  37987  ssbnd  38109  prdsbnd2  38116  cnpwstotbnd  38118  reheibor  38160  diophin  43204  fnwe2lem2  43479  dvsid  44758  limcresiooub  46070  limcresioolb  46071  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem58  46592  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem93  46627  fourierdlem100  46634  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierdlem112  46646  fourierdlem114  46648  afvres  47620  afv2res  47687