Description: Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011) (Revised by Stefan O'Rear, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | coires1 | |- ( A o. ( _I |` B ) ) = ( A |` B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cocnvcnv1 | |- ( `' `' A o. _I ) = ( A o. _I ) |
|
2 | relcnv | |- Rel `' `' A |
|
3 | coi1 | |- ( Rel `' `' A -> ( `' `' A o. _I ) = `' `' A ) |
|
4 | 2 3 | ax-mp | |- ( `' `' A o. _I ) = `' `' A |
5 | 1 4 | eqtr3i | |- ( A o. _I ) = `' `' A |
6 | 5 | reseq1i | |- ( ( A o. _I ) |` B ) = ( `' `' A |` B ) |
7 | resco | |- ( ( A o. _I ) |` B ) = ( A o. ( _I |` B ) ) |
|
8 | 6 7 | eqtr3i | |- ( `' `' A |` B ) = ( A o. ( _I |` B ) ) |
9 | rescnvcnv | |- ( `' `' A |` B ) = ( A |` B ) |
|
10 | 8 9 | eqtr3i | |- ( A o. ( _I |` B ) ) = ( A |` B ) |