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	⊢ ( 𝐴 ∘ ( I ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cocnvcnv1	⊢ ( ◡ ◡ 𝐴 ∘ I ) = ( 𝐴 ∘ I )
2		relcnv	⊢ Rel ◡ ◡ 𝐴
3		coi1	⊢ ( Rel ◡ ◡ 𝐴 → ( ◡ ◡ 𝐴 ∘ I ) = ◡ ◡ 𝐴 )
4	2 3	ax-mp	⊢ ( ◡ ◡ 𝐴 ∘ I ) = ◡ ◡ 𝐴
5	1 4	eqtr3i	⊢ ( 𝐴 ∘ I ) = ◡ ◡ 𝐴
6	5	reseq1i	⊢ ( ( 𝐴 ∘ I ) ↾ 𝐵 ) = ( ◡ ◡ 𝐴 ↾ 𝐵 )
7		resco	⊢ ( ( 𝐴 ∘ I ) ↾ 𝐵 ) = ( 𝐴 ∘ ( I ↾ 𝐵 ) )
8	6 7	eqtr3i	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ∘ ( I ↾ 𝐵 ) )
9		rescnvcnv	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 )
10	8 9	eqtr3i	⊢ ( 𝐴 ∘ ( I ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )