Theorem cocnv1ssid

Description: Characterizing when the composition of a converse with a class is included in the identity relation. The instance where the two classes are equal gives a characterization of injectivity (see df-f1 ). (Contributed by BJ, 22-Oct-2026)

	Ref	Expression
Assertion	cocnv1ssid	$$⊢B^{-1}\circ A\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge zBy\right)\to x=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		cocnv1ss	$$⊢B^{-1}\circ A\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge zBy\right)\to x\mathrm{I}z\right)$$
2		vex	$$⊢z\in \mathrm{V}$$
3	2	ideq	$$⊢x\mathrm{I}z\leftrightarrow x=z$$
4	3	imbi2i	$$⊢\left(\left(xAy\wedge zBy\right)\to x\mathrm{I}z\right)\leftrightarrow \left(\left(xAy\wedge zBy\right)\to x=z\right)$$
5	4	3albii	$$⊢\forall x\forall y\forall z\left(\left(xAy\wedge zBy\right)\to x\mathrm{I}z\right)\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge zBy\right)\to x=z\right)$$
6	1 5	bitri	$$⊢B^{-1}\circ A\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge zBy\right)\to x=z\right)$$