Theorem unidmex

Description: If F is a set, then U. dom F is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	unidmex.f	|- ( ph -> F e. V )
	unidmex.x	|- X = U. dom F
Assertion	unidmex	|- ( ph -> X e. _V )

Proof

Step	Hyp	Ref	Expression
1		unidmex.f	|- ( ph -> F e. V )
2		unidmex.x	|- X = U. dom F
3		dmexg	|- ( F e. V -> dom F e. _V )
4		uniexg	|- ( dom F e. _V -> U. dom F e. _V )
5	1 3 4	3syl	|- ( ph -> U. dom F e. _V )
6	2 5	eqeltrid	|- ( ph -> X e. _V )