Metamath Proof Explorer

Theorem unexg

Description: A union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16. (Contributed by NM, 18-Sep-2006)

Ref Expression
Assertion unexg A V B W A B V


Step Hyp Ref Expression
1 elex A V A V
2 elex B W B V
3 unexb A V B V A B V
4 3 biimpi A V B V A B V
5 1 2 4 syl2an A V B W A B V