Theorem coi1res

Description: Precomposing with the identity is the same as taking the relation part of a class. (Contributed by BJ, 16-Aug-2026)

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

Proof

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