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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	unidmex.x	⊢ 𝑋 = ∪ dom 𝐹
Assertion	unidmex	⊢ ( 𝜑 → 𝑋 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		unidmex.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		unidmex.x	⊢ 𝑋 = ∪ dom 𝐹
3		dmexg	⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
4		uniexg	⊢ ( dom 𝐹 ∈ V → ∪ dom 𝐹 ∈ V )
5	1 3 4	3syl	⊢ ( 𝜑 → ∪ dom 𝐹 ∈ V )
6	2 5	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ V )