![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resabs1 | Structured version Visualization version Unicode 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 5116 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sseqin2 3650 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | reseq2 5099 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylbi 199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | syl5eq 2496 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-opab 4461 df-xp 4839 df-rel 4840 df-res 4845 |
This theorem is referenced by: resabs1d 5133 resabs2 5134 resiima 5181 fun2ssres 5622 fssres2 5749 smores3 7069 setsres 15144 gsum2dlem2 17596 lindsss 19375 resthauslem 20372 ptcmpfi 20821 tsmsres 21151 ressxms 21533 nrginvrcn 21687 xrge0gsumle 21844 lebnumii 21990 dfrelog 23508 relogf1o 23509 dvlog 23589 dvlog2 23591 efopnlem2 23595 wilthlem2 23987 gsumle 28535 rrhre 28818 iwrdsplit 29213 cvmsss2 29990 mbfposadd 31981 mzpcompact2lem 35587 eldioph2 35598 diophin 35609 diophrex 35612 2rexfrabdioph 35633 3rexfrabdioph 35634 4rexfrabdioph 35635 6rexfrabdioph 35636 7rexfrabdioph 35637 dvmptresicc 37785 fourierdlem46 38010 fourierdlem57 38021 fourierdlem111 38075 fouriersw 38089 psmeasurelem 38302 |
Copyright terms: Public domain | W3C validator |