releccnveq

Description: Equality of converse R -coset and converse S -coset when R and S are relations. (Contributed by Peter Mazsa, 27-Jul-2019)

		Ref	Expression
	Assertion	releccnveq	$⊢ (Rel R \land Rel S) \to ([A] R^{-1} = [B] S^{-1} \leftrightarrow \forall x (x R A \leftrightarrow x S B))$

Step	Hyp	Ref	Expression
1		dfcleq	$⊢ [A] R^{-1} = [B] S^{-1} \leftrightarrow \forall x (x \in [A] R^{-1} \leftrightarrow x \in [B] S^{-1})$
2		releleccnv	$⊢ Rel R \to (x \in [A] R^{-1} \leftrightarrow x R A)$
3		releleccnv	$⊢ Rel S \to (x \in [B] S^{-1} \leftrightarrow x S B)$
4	2 3	bi2bian9	$⊢ (Rel R \land Rel S) \to ((x \in [A] R^{-1} \leftrightarrow x \in [B] S^{-1}) \leftrightarrow (x R A \leftrightarrow x S B))$
5	4	albidv	$⊢ (Rel R \land Rel S) \to (\forall x (x \in [A] R^{-1} \leftrightarrow x \in [B] S^{-1}) \leftrightarrow \forall x (x R A \leftrightarrow x S B))$
6	1 5	bitrid	$⊢ (Rel R \land Rel S) \to ([A] R^{-1} = [B] S^{-1} \leftrightarrow \forall x (x R A \leftrightarrow x S B))$

Metamath Proof Explorer