Theorem resabs1d 5975

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  f2ndf  8072  frrlem12  8249  ablfac1eulem  20015  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  kgencn2  23513  tsmsres  24100  resubmet  24758  xrge0gsumle  24790  cmssmscld  25318  cmsss  25319  cmscsscms  25341  minveclem3a  25395  dvmptresicc  25885  dvlip2  25968  c1liplem1  25969  efcvx  26427  logccv  26640  loglesqrt  26739  wilthlem2  27047  nosupno  27683  nosupbnd1lem1  27688  nosupbnd2  27696  noinfno  27698  noinfbnd1lem1  27703  noinfbnd2  27711  symgcom2  33177  cyc3conja  33250  bnj1280  35195  cvmlift2lem9  35524  mbfresfi  37911  ssbnd  38033  prdsbnd2  38040  cnpwstotbnd  38042  reheibor  38084  diophin  43123  fnwe2lem2  43402  dvsid  44681  limcresiooub  45994  limcresioolb  45995  fourierdlem46  46504  fourierdlem48  46506  fourierdlem49  46507  fourierdlem58  46516  fourierdlem72  46530  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem93  46551  fourierdlem100  46558  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem107  46565  fourierdlem111  46569  fourierdlem112  46570  fourierdlem114  46572  afvres  47526  afv2res  47593