Metamath Proof Explorer

Theorem cnvex

Description: The converse of a set is a set. Corollary 6.8(1) of TakeutiZaring p. 26. (Contributed by NM, 19-Dec-2003)

Ref Expression
Hypothesis cnvex.1 
|- A e. _V
Assertion cnvex 
|- `' A e. _V

Proof

Step Hyp Ref Expression
1 cnvex.1 
 |-  A e. _V
2 cnvexg 
 |-  ( A e. _V -> `' A e. _V )
3 1 2 ax-mp 
 |-  `' A e. _V