Theorem coires2

Description: Postcomposing with a restricted identity relation is the same as corestricting. (Contributed by BJ, 1-Nov-2026)

	Ref	Expression
Assertion	coires2	|- ( ( _I |` B ) o. A ) = ( A i^i ( _V X. B ) )

Proof

Step	Hyp	Ref	Expression
1		cnvresid	|- `' ( _I |` B ) = ( _I |` B )
2	1	coeq1i	|- ( `' ( _I |` B ) o. `' `' A ) = ( ( _I |` B ) o. `' `' A )
3		coires1	|- ( `' A o. ( _I |` B ) ) = ( `' A |` B )
4	3	cnveqi	|- `' ( `' A o. ( _I |` B ) ) = `' ( `' A |` B )
5		cnvco	|- `' ( `' A o. ( _I |` B ) ) = ( `' ( _I |` B ) o. `' `' A )
6		cnvrescnv	|- `' ( `' A |` B ) = ( A i^i ( _V X. B ) )
7	4 5 6	3eqtr3i	|- ( `' ( _I |` B ) o. `' `' A ) = ( A i^i ( _V X. B ) )
8		cocnvcnv2	|- ( ( _I |` B ) o. `' `' A ) = ( ( _I |` B ) o. A )
9	2 7 8	3eqtr3ri	|- ( ( _I |` B ) o. A ) = ( A i^i ( _V X. B ) )