Metamath Proof Explorer

Theorem unex

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 V
unex.2 B V
Assertion unex A B V


Step Hyp Ref Expression
1 unex.1 A V
2 unex.2 B V
3 1 2 unipr A B = A B
4 prex A B V
5 4 uniex A B V
6 3 5 eqeltrri A B V