Metamath Proof Explorer


Theorem unexg

Description: The union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16. (Contributed by NM, 18-Sep-2006) Prove unexg first and then unex and unexb from it. (Revised by BJ, 21-Jul-2025)

Ref Expression
Assertion unexg A V B W A B V

Proof

Step Hyp Ref Expression
1 uniprg A V B W A B = A B
2 prex A B V
3 2 a1i A V B W A B V
4 3 uniexd A V B W A B V
5 1 4 eqeltrrd A V B W A B V