Theorem 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 /\ Rel S ) -> ( [ A ] `' R = [ B ] `' S <-> A. x ( x R A <-> x S B ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( [ A ] `' R = [ B ] `' S <-> A. x ( x e. [ A ] `' R <-> x e. [ B ] `' S ) )
2		releleccnv	|- ( Rel R -> ( x e. [ A ] `' R <-> x R A ) )
3		releleccnv	|- ( Rel S -> ( x e. [ B ] `' S <-> x S B ) )
4	2 3	bi2bian9	|- ( ( Rel R /\ Rel S ) -> ( ( x e. [ A ] `' R <-> x e. [ B ] `' S ) <-> ( x R A <-> x S B ) ) )
5	4	albidv	|- ( ( Rel R /\ Rel S ) -> ( A. x ( x e. [ A ] `' R <-> x e. [ B ] `' S ) <-> A. x ( x R A <-> x S B ) ) )
6	1 5	syl5bb	|- ( ( Rel R /\ Rel S ) -> ( [ A ] `' R = [ B ] `' S <-> A. x ( x R A <-> x S B ) ) )