Theorem resabs1d 5679

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

Syntax hints:   → wi 4   = wceq 1601   ⊆ wss 3792   ↾ cres 5359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-opab 4951  df-xp 5363  df-rel 5364  df-res 5369

This theorem is referenced by:  f2ndf  7566  ablfac1eulem  18862  kgencn2  21773  tsmsres  22359  resubmet  23017  xrge0gsumle  23048  cmssmscld  23560  cmsss  23561  cmscsscms  23583  minveclem3a  23637  dvlip2  24199  c1liplem1  24200  efcvx  24644  logccv  24850  loglesqrt  24943  wilthlem2  25251  bnj1280  31691  cvmlift2lem9  31896  nosupno  32442  nosupbnd1lem1  32447  nosupbnd2  32455  mbfresfi  34086  ssbnd  34216  prdsbnd2  34223  cnpwstotbnd  34225  reheibor  34267  diophin  38306  fnwe2lem2  38590  dvsid  39496  limcresiooub  40792  limcresioolb  40793  dvmptresicc  41072  fourierdlem46  41306  fourierdlem48  41308  fourierdlem49  41309  fourierdlem58  41318  fourierdlem72  41332  fourierdlem73  41333  fourierdlem74  41334  fourierdlem75  41335  fourierdlem89  41349  fourierdlem90  41350  fourierdlem91  41351  fourierdlem93  41353  fourierdlem100  41360  fourierdlem102  41362  fourierdlem103  41363  fourierdlem104  41364  fourierdlem107  41367  fourierdlem111  41371  fourierdlem112  41372  fourierdlem114  41374  afvres  42223  afv2res  42290  funcrngcsetc  43023  funcrngcsetcALT  43024  funcringcsetc  43060