Theorem resabs1d 5954

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3898   ↾ cres 5622

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5155  df-xp 5626  df-rel 5627  df-res 5632

This theorem is referenced by:  f2ndf  8028  frrlem12  8183  ablfac1eulem  19770  kgencn2  22814  tsmsres  23401  resubmet  24071  xrge0gsumle  24102  cmssmscld  24620  cmsss  24621  cmscsscms  24643  minveclem3a  24697  dvmptresicc  25186  dvlip2  25265  c1liplem1  25266  efcvx  25714  logccv  25924  loglesqrt  26017  wilthlem2  26324  nosupno  26957  nosupbnd1lem1  26962  nosupbnd2  26970  noinfno  26972  noinfbnd1lem1  26977  noinfbnd2  26985  symgcom2  31640  cyc3conja  31711  bnj1280  33299  cvmlift2lem9  33572  mbfresfi  35936  ssbnd  36059  prdsbnd2  36066  cnpwstotbnd  36068  reheibor  36110  diophin  40864  fnwe2lem2  41147  dvsid  42278  limcresiooub  43527  limcresioolb  43528  fourierdlem46  44037  fourierdlem48  44039  fourierdlem49  44040  fourierdlem58  44049  fourierdlem72  44063  fourierdlem73  44064  fourierdlem74  44065  fourierdlem75  44066  fourierdlem89  44080  fourierdlem90  44081  fourierdlem91  44082  fourierdlem93  44084  fourierdlem100  44091  fourierdlem102  44093  fourierdlem103  44094  fourierdlem104  44095  fourierdlem107  44098  fourierdlem111  44102  fourierdlem112  44103  fourierdlem114  44105  afvres  45023  afv2res  45090  funcrngcsetc  45915  funcrngcsetcALT  45916  funcringcsetc  45952