Theorem dmexg

Description: The domain of a set is a set. Corollary 6.8(2) of TakeutiZaring p. 26. (Contributed by NM, 7-Apr-1995)

	Ref	Expression
Assertion	dmexg	|- ( A e. V -> dom 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		ssun1	|- dom A C_ ( dom A u. ran A )
4		dmrnssfld	|- ( dom A u. ran A ) C_ U. U. A
5	3 4	sstri	|- dom A C_ U. U. A
6		ssexg	|- ( ( dom A C_ U. U. A /\ U. U. A e. _V ) -> dom A e. _V )
7	5 6	mpan	|- ( U. U. A e. _V -> dom A e. _V )
8	1 2 7	3syl	|- ( A e. V -> dom A e. _V )