Theorem cocnv2ssid

Description: Characterizing when the composition of a class with a converse is included in the identity relation. The instance where the two classes are equal gives a characterization of single-valuedness (that is, for a relation to be a function, see df-fun ). (Contributed by BJ, 22-Oct-2026)

	Ref	Expression
Assertion	cocnv2ssid	|- ( ( B o. `' A ) C_ _I <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x = z ) )

Proof

Step	Hyp	Ref	Expression
1		cocnv2ss	|- ( ( B o. `' A ) C_ _I <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x _I z ) )
2		vex	|- z e. _V
3	2	ideq	|- ( x _I z <-> x = z )
4	3	imbi2i	|- ( ( ( y A x /\ y B z ) -> x _I z ) <-> ( ( y A x /\ y B z ) -> x = z ) )
5	4	3albii	|- ( A. x A. y A. z ( ( y A x /\ y B z ) -> x _I z ) <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x = z ) )
6	1 5	bitri	|- ( ( B o. `' A ) C_ _I <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x = z ) )