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 )