Metamath Proof Explorer

Theorem opelcnvg

Description: Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion opelcnvg 
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )

Proof

Step Hyp Ref Expression
1 brcnvg 
 |-  ( ( A e. C /\ B e. D ) -> ( A `' R B <-> B R A ) )
2 df-br 
 |-  ( A `' R B <-> <. A , B >. e. `' R )
3 df-br 
 |-  ( B R A <-> <. B , A >. e. R )
4 1 2 3 3bitr3g 
 |-  ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )