Theorem resabs1d 5979

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644  df-rel 5645  df-res 5650

This theorem is referenced by:  f2ndf  8099  frrlem12  8276  ablfac1eulem  20004  funcrngcsetc  20549  funcrngcsetcALT  20550  funcringcsetc  20583  kgencn2  23444  tsmsres  24031  resubmet  24690  xrge0gsumle  24722  cmssmscld  25250  cmsss  25251  cmscsscms  25273  minveclem3a  25327  dvmptresicc  25817  dvlip2  25900  c1liplem1  25901  efcvx  26359  logccv  26572  loglesqrt  26671  wilthlem2  26979  nosupno  27615  nosupbnd1lem1  27620  nosupbnd2  27628  noinfno  27630  noinfbnd1lem1  27635  noinfbnd2  27643  symgcom2  33041  cyc3conja  33114  bnj1280  35010  cvmlift2lem9  35298  mbfresfi  37660  ssbnd  37782  prdsbnd2  37789  cnpwstotbnd  37791  reheibor  37833  diophin  42760  fnwe2lem2  43040  dvsid  44320  limcresiooub  45640  limcresioolb  45641  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem93  46197  fourierdlem100  46204  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierdlem112  46216  fourierdlem114  46218  afvres  47173  afv2res  47240