Metamath Proof Explorer

Theorem cosscnvelrels

Description: Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021)

Ref Expression
Assertion cosscnvelrels 
|- ( A e. V -> ,~ `' A e. Rels )

Proof

Step Hyp Ref Expression
1 cnvelrels 
 |-  ( A e. V -> `' A e. Rels )
2 cosselrels 
 |-  ( `' A e. Rels -> ,~ `' A e. Rels )
3 1 2 syl 
 |-  ( A e. V -> ,~ `' A e. Rels )