Theorem resabs1d 6011

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-xp 5661  df-rel 5662  df-res 5667

This theorem is used by:  f2ndf  8158  fnwe2lem3  8174  frrlem12  8343  ablfac1eulem  20318  funcrngcsetc  20922  funcrngcsetcALT  20923  funcringcsetc  20956  kgencn2  23906  tsmsres  24493  resubmet  25151  xrge0gsumle  25183  cmssmscld  25701  cmsss  25702  cmscsscms  25724  minveclem3a  25778  dvmptresicc  26266  dvlip2  26345  c1liplem1  26346  efcvx  26806  logccv  27021  loglesqrt  27119  wilthlem2  27426  nosupno  28090  nosupbnd1lem1  28095  nosupbnd2  28103  noinfno  28105  noinfbnd1lem1  28110  noinfbnd2  28118  symgcom2  33715  cyc3conja  33788  bnj1280  35720  cvmlift2lem9  36243  mbfresfi  38776  ssbnd  38914  prdsbnd2  38921  cnpwstotbnd  38923  reheibor  38965  diophin  43976  dvsid  45507  limcresiooub  46857  limcresioolb  46858  fourierdlem46  47367  fourierdlem48  47369  fourierdlem49  47370  fourierdlem58  47379  fourierdlem72  47393  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem93  47414  fourierdlem100  47421  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem107  47428  fourierdlem111  47432  fourierdlem112  47433  fourierdlem114  47435  afvres  48447  afv2res  48514