![]() |
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 5948 | . 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵)) | |
2 | sseqin2 4173 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵) | |
3 | reseq2 5930 | . . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) | |
4 | 2, 3 | sylbi 216 | . 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) |
5 | 1, 4 | eqtrid 2788 | 1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∩ cin 3907 ⊆ wss 3908 ↾ cres 5633 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-opab 5166 df-xp 5637 df-rel 5638 df-res 5643 |
This theorem is referenced by: resabs1d 5966 resabs2 5967 resiima 6026 fun2ssres 6543 fssres2 6707 smores3 8291 setsres 17004 gsum2dlem2 19701 lindsss 21177 resthauslem 22660 ptcmpfi 23110 tsmsres 23441 ressxms 23827 nrginvrcn 24002 xrge0gsumle 24142 lebnumii 24275 dvmptresicc 25226 dfrelog 25867 relogf1o 25868 dvlog 25952 dvlog2 25954 efopnlem2 25958 wilthlem2 26364 nosupres 27001 nosupbnd2lem1 27009 noinfres 27016 noinfbnd2lem1 27024 nosupinfsep 27026 gsumle 31774 rrhre 32430 iwrdsplit 32815 rpsqrtcn 33034 pthhashvtx 33549 cvmsss2 33696 mbfposadd 36057 mzpcompact2lem 40977 eldioph2 40988 diophin 40998 diophrex 41001 2rexfrabdioph 41022 3rexfrabdioph 41023 4rexfrabdioph 41024 6rexfrabdioph 41025 7rexfrabdioph 41026 resabs1i 43260 fourierdlem46 44288 fourierdlem57 44299 fourierdlem111 44353 fouriersw 44367 psmeasurelem 44606 |
Copyright terms: Public domain | W3C validator |