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 )