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 e. [ B ] `' R <-> A R B ) )

Proof

Step Hyp Ref Expression
1 relcnv
 |-  Rel `' R
2 relelec
 |-  ( Rel `' R -> ( A e. [ B ] `' R <-> B `' R A ) )
3 1 2 ax-mp
 |-  ( A e. [ B ] `' R <-> B `' R A )
4 relbrcnvg
 |-  ( Rel R -> ( B `' R A <-> A R B ) )
5 3 4 syl5bb
 |-  ( Rel R -> ( A e. [ B ] `' R <-> A R B ) )