Theorem resabs1d 5538

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

Syntax hints:   → wi 4   = wceq 1596   ⊆ wss 3680   ↾ cres 5220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-opab 4821  df-xp 5224  df-rel 5225  df-res 5230

This theorem is referenced by:  f2ndf  7403  ablfac1eulem  18592  kgencn2  21483  tsmsres  22069  resubmet  22727  xrge0gsumle  22758  cmsss  23268  minveclem3a  23319  dvlip2  23878  c1liplem1  23879  efcvx  24323  logccv  24529  loglesqrt  24619  wilthlem2  24915  bnj1280  31316  cvmlift2lem9  31521  nosupno  32076  nosupbnd1lem1  32081  nosupbnd2  32089  mbfresfi  33688  ssbnd  33819  prdsbnd2  33826  cnpwstotbnd  33828  reheibor  33870  diophin  37755  fnwe2lem2  38040  dvsid  38949  limcresiooub  40294  limcresioolb  40295  dvmptresicc  40554  fourierdlem46  40789  fourierdlem48  40791  fourierdlem49  40792  fourierdlem58  40801  fourierdlem72  40815  fourierdlem73  40816  fourierdlem74  40817  fourierdlem75  40818  fourierdlem89  40832  fourierdlem90  40833  fourierdlem91  40834  fourierdlem93  40836  fourierdlem100  40843  fourierdlem102  40845  fourierdlem103  40846  fourierdlem104  40847  fourierdlem107  40850  fourierdlem111  40854  fourierdlem112  40855  fourierdlem114  40857  afvres  41675  funcrngcsetc  42425  funcrngcsetcALT  42426  funcringcsetc  42462