Theorem resabs1d 5967

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890   ↾ cres 5626

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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  f2ndf  8063  frrlem12  8240  ablfac1eulem  20040  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  kgencn2  23532  tsmsres  24119  resubmet  24777  xrge0gsumle  24809  cmssmscld  25327  cmsss  25328  cmscsscms  25350  minveclem3a  25404  dvmptresicc  25893  dvlip2  25972  c1liplem1  25973  efcvx  26427  logccv  26640  loglesqrt  26738  wilthlem2  27046  nosupno  27681  nosupbnd1lem1  27686  nosupbnd2  27694  noinfno  27696  noinfbnd1lem1  27701  noinfbnd2  27709  symgcom2  33160  cyc3conja  33233  bnj1280  35178  cvmlift2lem9  35509  mbfresfi  38001  ssbnd  38123  prdsbnd2  38130  cnpwstotbnd  38132  reheibor  38174  diophin  43218  fnwe2lem2  43497  dvsid  44776  limcresiooub  46088  limcresioolb  46089  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem58  46610  fourierdlem72  46624  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem93  46645  fourierdlem100  46652  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem112  46664  fourierdlem114  46666  afvres  47632  afv2res  47699