Theorem resabs1d 6011

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3947   ↾ cres 5677

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-xp 5681  df-rel 5682  df-res 5687

This theorem is referenced by:  f2ndf  8108  frrlem12  8284  ablfac1eulem  19983  kgencn2  23281  tsmsres  23868  resubmet  24538  xrge0gsumle  24569  cmssmscld  25098  cmsss  25099  cmscsscms  25121  minveclem3a  25175  dvmptresicc  25665  dvlip2  25747  c1liplem1  25748  efcvx  26197  logccv  26407  loglesqrt  26502  wilthlem2  26809  nosupno  27442  nosupbnd1lem1  27447  nosupbnd2  27455  noinfno  27457  noinfbnd1lem1  27462  noinfbnd2  27470  symgcom2  32515  cyc3conja  32586  bnj1280  34329  cvmlift2lem9  34600  mbfresfi  36837  ssbnd  36959  prdsbnd2  36966  cnpwstotbnd  36968  reheibor  37010  diophin  41812  fnwe2lem2  42095  dvsid  43392  limcresiooub  44656  limcresioolb  44657  fourierdlem46  45166  fourierdlem48  45168  fourierdlem49  45169  fourierdlem58  45178  fourierdlem72  45192  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fourierdlem93  45213  fourierdlem100  45220  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  fourierdlem111  45231  fourierdlem112  45232  fourierdlem114  45234  afvres  46178  afv2res  46245  funcrngcsetc  46984  funcrngcsetcALT  46985  funcringcsetc  47021