Metamath Proof Explorer


Theorem releleccnv

Description: Elementhood in a converse R -coset when R is a relation. (Contributed by Peter Mazsa, 9-Dec-2018)

Ref Expression
Assertion releleccnv Rel R A B R -1 A R B

Proof

Step Hyp Ref Expression
1 relcnv Rel R -1
2 relelec Rel R -1 A B R -1 B R -1 A
3 1 2 ax-mp A B R -1 B R -1 A
4 relbrcnvg Rel R B R -1 A A R B
5 3 4 syl5bb Rel R A B R -1 A R B