![]() |
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 5995 | . 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵)) | |
2 | sseqin2 4216 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵) | |
3 | reseq2 5977 | . . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) | |
4 | 2, 3 | sylbi 216 | . 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) |
5 | 1, 4 | eqtrid 2785 | 1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∩ cin 3948 ⊆ wss 3949 ↾ cres 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-opab 5212 df-xp 5683 df-rel 5684 df-res 5689 |
This theorem is referenced by: resabs1d 6013 resabs2 6014 resiima 6076 fun2ssres 6594 fssres2 6760 smores3 8353 setsres 17111 gsum2dlem2 19839 lindsss 21379 resthauslem 22867 ptcmpfi 23317 tsmsres 23648 ressxms 24034 nrginvrcn 24209 xrge0gsumle 24349 lebnumii 24482 dvmptresicc 25433 dfrelog 26074 relogf1o 26075 dvlog 26159 dvlog2 26161 efopnlem2 26165 wilthlem2 26573 nosupres 27210 nosupbnd2lem1 27218 noinfres 27225 noinfbnd2lem1 27233 nosupinfsep 27235 gsumle 32242 rrhre 33001 iwrdsplit 33386 rpsqrtcn 33605 pthhashvtx 34118 cvmsss2 34265 mbfposadd 36535 mzpcompact2lem 41489 eldioph2 41500 diophin 41510 diophrex 41513 2rexfrabdioph 41534 3rexfrabdioph 41535 4rexfrabdioph 41536 6rexfrabdioph 41537 7rexfrabdioph 41538 resabs1i 43834 fourierdlem46 44868 fourierdlem57 44879 fourierdlem111 44933 fouriersw 44947 psmeasurelem 45186 |
Copyright terms: Public domain | W3C validator |