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 AV
unex.2 BV
Assertion unex ABV

Proof

Step Hyp Ref Expression
1 unex.1 AV
2 unex.2 BV
3 1 2 unipr AB=AB
4 prex ABV
5 4 uniex ABV
6 3 5 eqeltrri ABV