Theorem resabs1d 6005

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

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

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 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-xp 5665  df-rel 5666  df-res 5671

This theorem is used by:  f2ndf  8121  frrlem12  8300  ablfac1eulem  20207  funcrngcsetc  20808  funcrngcsetcALT  20809  funcringcsetc  20842  kgencn2  23789  tsmsres  24376  resubmet  25034  xrge0gsumle  25066  cmssmscld  25584  cmsss  25585  cmscsscms  25607  minveclem3a  25661  dvmptresicc  26150  dvlip2  26229  c1liplem1  26230  efcvx  26692  logccv  26908  loglesqrt  27006  wilthlem2  27313  nosupno  27947  nosupbnd1lem1  27952  nosupbnd2  27960  noinfno  27962  noinfbnd1lem1  27967  noinfbnd2  27975  symgcom2  33532  cyc3conja  33605  bnj1280  35537  cvmlift2lem9  35898  mbfresfi  38423  ssbnd  38546  prdsbnd2  38553  cnpwstotbnd  38555  reheibor  38597  diophin  43625  fnwe2lem2  43900  dvsid  45163  limcresiooub  46478  limcresioolb  46479  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem58  47000  fourierdlem72  47014  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem93  47035  fourierdlem100  47042  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  fourierdlem111  47053  fourierdlem112  47054  fourierdlem114  47056  afvres  48068  afv2res  48135