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 \in V$
	iunex.2	$⊢ B \in V$
Assertion	iunex	$⊢ ⋃_{x \in A} B \in V$

Proof

Step	Hyp	Ref	Expression
1		iunex.1	$⊢ A \in V$
2		iunex.2	$⊢ B \in V$
3	2	rgenw	$⊢ \forall x \in A B \in V$
4		iunexg	$⊢ (A \in V \land \forall x \in A B \in V) \to ⋃_{x \in A} B \in V$
5	1 3 4	mp2an	$⊢ ⋃_{x \in A} B \in V$