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

Metamath Proof Explorer

Theorem iunex

Description: The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B , which can be read informally as B ( x ) . (Contributed by NM, 13-Oct-2003)

Ref Expression
Hypotheses iunex.1 ⊢ A ∈ V
iunex.2 ⊢ B ∈ V
Assertion iunex ⊢ ⋃ x ∈ A B ∈ V

Proof

Step Hyp Ref Expression
1 iunex.1 ⊢ A ∈ V
2 iunex.2 ⊢ B ∈ V
3 2 rgenw ⊢ ∀ x ∈ A B ∈ V
4 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⋃ x ∈ A B ∈ V
5 1 3 4 mp2an ⊢ ⋃ x ∈ A B ∈ V