| 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 6010 | . 2 ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ (𝐶 ∩ 𝐵)) | |
| 2 | sseqin2 4223 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐶 ∩ 𝐵) = 𝐵) | |
| 3 | reseq2 5992 | . . 3 ⊢ ((𝐶 ∩ 𝐵) = 𝐵 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) | |
| 4 | 2, 3 | sylbi 217 | . 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐴 ↾ (𝐶 ∩ 𝐵)) = (𝐴 ↾ 𝐵)) |
| 5 | 1, 4 | eqtrid 2789 | 1 ⊢ (𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∩ cin 3950 ⊆ wss 3951 ↾ cres 5687 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-opab 5206 df-xp 5691 df-rel 5692 df-res 5697 |
| This theorem is referenced by: resabs1i 6025 resabs1d 6026 resabs2 6027 resiima 6094 fun2ssres 6611 fssres2 6776 smores3 8393 setsres 17215 gsum2dlem2 19989 lindsss 21844 resthauslem 23371 ptcmpfi 23821 tsmsres 24152 ressxms 24538 nrginvrcn 24713 xrge0gsumle 24855 lebnumii 24998 dvmptresicc 25951 dfrelog 26607 relogf1o 26608 dvlog 26693 dvlog2 26695 efopnlem2 26699 wilthlem2 27112 nosupres 27752 nosupbnd2lem1 27760 noinfres 27767 noinfbnd2lem1 27775 nosupinfsep 27777 gsumle 33101 rrhre 34022 iwrdsplit 34389 rpsqrtcn 34608 pthhashvtx 35133 cvmsss2 35279 mbfposadd 37674 mzpcompact2lem 42762 eldioph2 42773 diophin 42783 diophrex 42786 2rexfrabdioph 42807 3rexfrabdioph 42808 4rexfrabdioph 42809 6rexfrabdioph 42810 7rexfrabdioph 42811 fourierdlem46 46167 fourierdlem57 46178 fourierdlem111 46232 fouriersw 46246 psmeasurelem 46485 |
| Copyright terms: Public domain | W3C validator |