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 e. V /\ B e. W ) -> ( A u. B ) e. _V )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 elex 
 |-  ( B e. W -> B e. _V )
3 unexb 
 |-  ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
4 3 biimpi 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
5 1 2 4 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )