Metamath Proof Explorer


Theorem coires1

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 )

Proof

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 )