This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )