Description: The union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16. (Contributed by NM, 1-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Hypotheses | unex.1 | |- A e. _V |
|
unex.2 | |- B e. _V |
||
Assertion | unex | |- ( A u. B ) e. _V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unex.1 | |- A e. _V |
|
2 | unex.2 | |- B e. _V |
|
3 | unexg | |- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V ) |
|
4 | 1 2 3 | mp2an | |- ( A u. B ) e. _V |