Theorem resabs1d 6012

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 18	1 ⊢ (𝜑 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3908   ↾ cres 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-xp 5672  df-rel 5673  df-res 5678

This theorem is used by:  f2ndf  8124  frrlem12  8303  ablfac1eulem  20175  funcrngcsetc  20776  funcrngcsetcALT  20777  funcringcsetc  20810  kgencn2  23751  tsmsres  24338  resubmet  24996  xrge0gsumle  25028  cmssmscld  25546  cmsss  25547  cmscsscms  25569  minveclem3a  25623  dvmptresicc  26112  dvlip2  26191  c1liplem1  26192  efcvx  26649  logccv  26865  loglesqrt  26963  wilthlem2  27270  nosupno  27904  nosupbnd1lem1  27909  nosupbnd2  27917  noinfno  27919  noinfbnd1lem1  27924  noinfbnd2  27932  symgcom2  33435  cyc3conja  33508  bnj1280  35439  cvmlift2lem9  35823  mbfresfi  38357  ssbnd  38479  prdsbnd2  38486  cnpwstotbnd  38488  reheibor  38530  diophin  43543  fnwe2lem2  43818  dvsid  45081  limcresiooub  46396  limcresioolb  46397  fourierdlem46  46906  fourierdlem48  46908  fourierdlem49  46909  fourierdlem58  46918  fourierdlem72  46932  fourierdlem73  46933  fourierdlem74  46934  fourierdlem75  46935  fourierdlem89  46949  fourierdlem90  46950  fourierdlem91  46951  fourierdlem93  46953  fourierdlem100  46960  fourierdlem102  46962  fourierdlem103  46963  fourierdlem104  46964  fourierdlem107  46967  fourierdlem111  46971  fourierdlem112  46972  fourierdlem114  46974  afvres  47949  afv2res  48016