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 1541   ⊆ wss 3901   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  f2ndf  8062  frrlem12  8239  ablfac1eulem  20003  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  kgencn2  23501  tsmsres  24088  resubmet  24746  xrge0gsumle  24778  cmssmscld  25306  cmsss  25307  cmscsscms  25329  minveclem3a  25383  dvmptresicc  25873  dvlip2  25956  c1liplem1  25957  efcvx  26415  logccv  26628  loglesqrt  26727  wilthlem2  27035  nosupno  27671  nosupbnd1lem1  27676  nosupbnd2  27684  noinfno  27686  noinfbnd1lem1  27691  noinfbnd2  27699  symgcom2  33166  cyc3conja  33239  bnj1280  35176  cvmlift2lem9  35505  mbfresfi  37863  ssbnd  37985  prdsbnd2  37992  cnpwstotbnd  37994  reheibor  38036  diophin  43010  fnwe2lem2  43289  dvsid  44568  limcresiooub  45882  limcresioolb  45883  fourierdlem46  46392  fourierdlem48  46394  fourierdlem49  46395  fourierdlem58  46404  fourierdlem72  46418  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem93  46439  fourierdlem100  46446  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem107  46453  fourierdlem111  46457  fourierdlem112  46458  fourierdlem114  46460  afvres  47414  afv2res  47481