This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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