Metamath Proof Explorer


Theorem brtrclfvcnv

Description: Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020)

Ref Expression
Assertion brtrclfvcnv RVAt+R-1BrR-1rrrrArB

Proof

Step Hyp Ref Expression
1 cnvexg RVR-1V
2 brtrclfv R-1VAt+R-1BrR-1rrrrArB
3 1 2 syl RVAt+R-1BrR-1rrrrArB