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 ⊢ φ → F ∈ V
unidmex.x ⊢ X = ⋃ dom ⁡ F
Assertion unidmex ⊢ φ → X ∈ V

Proof

Step Hyp Ref Expression
1 unidmex.f ⊢ φ → F ∈ V
2 unidmex.x ⊢ X = ⋃ dom ⁡ F
3 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
4 uniexg ⊢ dom ⁡ F ∈ V → ⋃ dom ⁡ F ∈ V
5 1 3 4 3syl ⊢ φ → ⋃ dom ⁡ F ∈ V
6 2 5 eqeltrid ⊢ φ → X ∈ V