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