This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvexg

Description: The converse of a set is a set. Corollary 6.8(1) of TakeutiZaring p. 26. (Contributed by NM, 17-Mar-1998)

Ref Expression
Assertion cnvexg 
|- ( A e. V -> `' A e. _V )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' A
2 relssdmrn 
 |-  ( Rel `' A -> `' A C_ ( dom `' A X. ran `' A ) )
3 1 2 ax-mp 
 |-  `' A C_ ( dom `' A X. ran `' A )
4 df-rn 
 |-  ran A = dom `' A
5 rnexg 
 |-  ( A e. V -> ran A e. _V )
6 4 5 eqeltrrid 
 |-  ( A e. V -> dom `' A e. _V )
7 dfdm4 
 |-  dom A = ran `' A
8 dmexg 
 |-  ( A e. V -> dom A e. _V )
9 7 8 eqeltrrid 
 |-  ( A e. V -> ran `' A e. _V )
10 6 9 xpexd 
 |-  ( A e. V -> ( dom `' A X. ran `' A ) e. _V )
11 ssexg 
 |-  ( ( `' A C_ ( dom `' A X. ran `' A ) /\ ( dom `' A X. ran `' A ) e. _V ) -> `' A e. _V )
12 3 10 11 sylancr 
 |-  ( A e. V -> `' A e. _V )