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 e. V -> `' A e. Rels )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' A
2 cnvexg 
 |-  ( A e. V -> `' A e. _V )
3 elrelsrel 
 |-  ( `' A e. _V -> ( `' A e. Rels <-> Rel `' A ) )
4 2 3 syl 
 |-  ( A e. V -> ( `' A e. Rels <-> Rel `' A ) )
5 1 4 mpbiri 
 |-  ( A e. V -> `' A e. Rels )