cocnv1ss

Description: Characterizing when the composition of a converse with a class is included in another. (Contributed by BJ, 22-Oct-2026)

		Ref	Expression
	Assertion	cocnv1ss	$⊢ B^{-1} \circ A \subseteq C \leftrightarrow \forall x \forall y \forall z ((x A y \land z B y) \to x C z)$

Step	Hyp	Ref	Expression
1		cotrg	$⊢ B^{-1} \circ A \subseteq C \leftrightarrow \forall x \forall y \forall z ((x A y \land y B^{-1} z) \to x C z)$
2		vex	$⊢ y \in V$
3		vex	$⊢ z \in V$
4	2 3	brcnv	$⊢ y B^{-1} z \leftrightarrow z B y$
5	4	anbi2i	$⊢ (x A y \land y B^{-1} z) \leftrightarrow (x A y \land z B y)$
6	5	imbi1i	$⊢ ((x A y \land y B^{-1} z) \to x C z) \leftrightarrow ((x A y \land z B y) \to x C z)$
7	6	3albii	$⊢ \forall x \forall y \forall z ((x A y \land y B^{-1} z) \to x C z) \leftrightarrow \forall x \forall y \forall z ((x A y \land z B y) \to x C z)$
8	1 7	bitri	$⊢ B^{-1} \circ A \subseteq C \leftrightarrow \forall x \forall y \forall z ((x A y \land z B y) \to x C z)$

Metamath Proof Explorer