Metamath Proof Explorer


Theorem cnvelrels

Description: The converse of a set is an element of the class of relations. (Contributed by Peter Mazsa, 18-Aug-2019)

Ref Expression
Assertion cnvelrels A V A -1 Rels

Proof

Step Hyp Ref Expression
1 relcnv Rel A -1
2 cnvexg A V A -1 V
3 elrelsrel A -1 V A -1 Rels Rel A -1
4 2 3 syl A V A -1 Rels Rel A -1
5 1 4 mpbiri A V A -1 Rels