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 C B D A B R -1 B A R

Proof

Step Hyp Ref Expression
1 brcnvg A C B D A R -1 B B R A
2 df-br A R -1 B A B R -1
3 df-br B R A B A R
4 1 2 3 3bitr3g A C B D A B R -1 B A R