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	$$⊢\phi \to F\in V$$
	unidmex.x	$$⊢X=\bigcup \mathrm{dom}F$$
Assertion	unidmex	$$⊢\phi \to X\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		unidmex.f	$$⊢\phi \to F\in V$$
2		unidmex.x	$$⊢X=\bigcup \mathrm{dom}F$$
3		dmexg	$$⊢F\in V\to \mathrm{dom}F\in \mathrm{V}$$
4		uniexg	$$⊢\mathrm{dom}F\in \mathrm{V}\to \bigcup \mathrm{dom}F\in \mathrm{V}$$
5	1 3 4	3syl	$$⊢\phi \to \bigcup \mathrm{dom}F\in \mathrm{V}$$
6	2 5	eqeltrid	$$⊢\phi \to X\in \mathrm{V}$$