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


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