Theorem relpart

Description: Two ways of expressing the "relation part" of a class: its restriction to the universal class (that is, its intersection with the Cartesian square of the universal class) equals the class of ordered pairs it contains (the class of ordered pairs whose components are related by it).

The "relation part" of a class is a relation (see df-rel and relres ) and is the largest relation included in that class (that follows from relssresv ). Taking the relation part of a class is a projection onto the collection of relations, that is, it is an idempotent operation ( residm ) with image the collection of relations (by relres for one inclusion and the forward implication of dfrel3 for the other). As with any projection, a class is in its image if and only if its is a fixpoint of that projection (which is precisely dfrel3 ).

Other expressions giving the relation part of a class are cnvcnv , coi1res . (Contributed by BJ, 16-Oct-2026)

	Ref	Expression
Assertion	relpart	|- ( A |` _V ) = { <. x , y >. | x A y }

Proof

Step	Hyp	Ref	Expression
1		bj-dfres2	|- ( A |` _V ) = { <. x , y >. | ( x e. _V /\ x A y ) }
2		vex	|- x e. _V
3	2	biantrur	|- ( x A y <-> ( x e. _V /\ x A y ) )
4	3	bicomi	|- ( ( x e. _V /\ x A y ) <-> x A y )
5	4	opabbii	|- { <. x , y >. | ( x e. _V /\ x A y ) } = { <. x , y >. | x A y }
6	1 5	eqtri	|- ( A |` _V ) = { <. x , y >. | x A y }