Metamath Proof Explorer

Theorem cosscnvex

Description: If A is a set then the class of cosets by the converse of A is a set. (Contributed by Peter Mazsa, 18-Oct-2019)

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

Proof

Step Hyp Ref Expression
1 cnvexg 
 |-  ( A e. V -> `' A e. _V )
2 cossex 
 |-  ( `' A e. _V -> ,~ `' A e. _V )
3 1 2 syl 
 |-  ( A e. V -> ,~ `' A e. _V )