Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resabs1 | Structured version Visualization version GIF version |
Description: Absorption law for restriction. Exercise 17 of [TakeutiZaring] p. 25. (Contributed by NM, 9-Aug-1994.) |
Ref | Expression |
---|---|
resabs1 | ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resres 5859 | . 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵)) | |
2 | sseqin2 4189 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵) | |
3 | reseq2 5841 | . . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) | |
4 | 2, 3 | sylbi 218 | . 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) |
5 | 1, 4 | syl5eq 2865 | 1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∩ cin 3932 ⊆ wss 3933 ↾ cres 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-opab 5120 df-xp 5554 df-rel 5555 df-res 5560 |
This theorem is referenced by: resabs1d 5877 resabs2 5878 resiima 5937 fun2ssres 6392 fssres2 6539 smores3 7979 setsres 16513 gsum2dlem2 19020 lindsss 20896 resthauslem 21899 ptcmpfi 22349 tsmsres 22679 ressxms 23062 nrginvrcn 23228 xrge0gsumle 23368 lebnumii 23497 dfrelog 25076 relogf1o 25077 dvlog 25161 dvlog2 25163 efopnlem2 25167 wilthlem2 25573 gsumle 30652 rrhre 31161 iwrdsplit 31544 rpsqrtcn 31763 pthhashvtx 32271 cvmsss2 32418 nosupres 33104 nosupbnd2lem1 33112 mbfposadd 34820 mzpcompact2lem 39226 eldioph2 39237 diophin 39247 diophrex 39250 2rexfrabdioph 39271 3rexfrabdioph 39272 4rexfrabdioph 39273 6rexfrabdioph 39274 7rexfrabdioph 39275 resabs1i 41290 dvmptresicc 42080 fourierdlem46 42314 fourierdlem57 42325 fourierdlem111 42379 fouriersw 42393 psmeasurelem 42629 |
Copyright terms: Public domain | W3C validator |