Theorem coi2res

Description: Postcomposing with the identity is the same as taking the relation part of a class. See also coi1res and coires2 . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coi2res	|- ( _I o. A ) = ( A |` _V )

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2	1	ideq	|- ( z _I y <-> z = y )
3	2	anbi2i	|- ( ( x A z /\ z _I y ) <-> ( x A z /\ z = y ) )
4		ancom	|- ( ( x A z /\ z = y ) <-> ( z = y /\ x A z ) )
5	3 4	bitri	|- ( ( x A z /\ z _I y ) <-> ( z = y /\ x A z ) )
6	5	exbii	|- ( E. z ( x A z /\ z _I y ) <-> E. z ( z = y /\ x A z ) )
7		breq2	|- ( z = y -> ( x A z <-> x A y ) )
8	7	equsexvw	|- ( E. z ( z = y /\ x A z ) <-> x A y )
9	6 8	bitri	|- ( E. z ( x A z /\ z _I y ) <-> x A y )
10	9	opabbii	|- { <. x , y >. | E. z ( x A z /\ z _I y ) } = { <. x , y >. | x A y }
11		df-co	|- ( _I o. A ) = { <. x , y >. | E. z ( x A z /\ z _I y ) }
12		relpart	|- ( A |` _V ) = { <. x , y >. | x A y }
13	10 11 12	3eqtr4i	|- ( _I o. A ) = ( A |` _V )