Theorem bj-cossid

Description: Characterizing when the composition of two classes is included in the identity relation. The instance where the two classes are equal gives a characterization of sub-involutivity (see nvo ). (Contributed by BJ, 22-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		cotrg	$$⊢B\circ A\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge yBz\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 yBz\right)\to x\mathrm{I}z\right)\leftrightarrow \left(\left(xAy\wedge yBz\right)\to x=z\right)$$
5	4	3albii	$$⊢\forall x\forall y\forall z\left(\left(xAy\wedge yBz\right)\to x\mathrm{I}z\right)\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge yBz\right)\to x=z\right)$$
6	1 5	bitri	$$⊢B\circ A\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\forall z\left(\left(xAy\wedge yBz\right)\to x=z\right)$$