Theorem resabs1d 5998

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-xp 5656  df-rel 5657  df-res 5662

This theorem is used by:  f2ndf  8133  fnwe2lem3  8149  frrlem12  8318  ablfac1eulem  20293  funcrngcsetc  20897  funcrngcsetcALT  20898  funcringcsetc  20931  kgencn2  23881  tsmsres  24468  resubmet  25126  xrge0gsumle  25158  cmssmscld  25676  cmsss  25677  cmscsscms  25699  minveclem3a  25753  dvmptresicc  26241  dvlip2  26320  c1liplem1  26321  efcvx  26781  logccv  26996  loglesqrt  27094  wilthlem2  27401  nosupno  28065  nosupbnd1lem1  28070  nosupbnd2  28078  noinfno  28080  noinfbnd1lem1  28085  noinfbnd2  28093  symgcom2  33691  cyc3conja  33764  bnj1280  35696  cvmlift2lem9  36162  mbfresfi  38677  ssbnd  38815  prdsbnd2  38822  cnpwstotbnd  38824  reheibor  38866  diophin  43876  dvsid  45408  limcresiooub  46745  limcresioolb  46746  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem58  47267  fourierdlem72  47281  fourierdlem73  47282  fourierdlem74  47283  fourierdlem75  47284  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem93  47302  fourierdlem100  47309  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem107  47316  fourierdlem111  47320  fourierdlem112  47321  fourierdlem114  47323  afvres  48335  afv2res  48402