Theorem rnexg

Description: The range of a set is a set. Corollary 6.8(3) of TakeutiZaring p. 26. Similar to Lemma 3D of Enderton p. 41. (Contributed by NM, 31-Mar-1995)

	Ref	Expression
Assertion	rnexg	|- ( A e. V -> ran A e. _V )

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( A e. V -> U. A e. _V )
2		uniexg	|- ( U. A e. _V -> U. U. A e. _V )
3		ssun2	|- ran A C_ ( dom A u. ran A )
4		dmrnssfld	|- ( dom A u. ran A ) C_ U. U. A
5	3 4	sstri	|- ran A C_ U. U. A
6		ssexg	|- ( ( ran A C_ U. U. A /\ U. U. A e. _V ) -> ran A e. _V )
7	5 6	mpan	|- ( U. U. A e. _V -> ran A e. _V )
8	1 2 7	3syl	|- ( A e. V -> ran A e. _V )