Theorem unexd

Description: The union of two sets is a set. (Contributed by SN, 16-Jul-2024)

	Ref	Expression
Hypotheses	unexd.1	|- ( ph -> A e. V )
	unexd.2	|- ( ph -> B e. W )
Assertion	unexd	|- ( ph -> ( A u. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		unexd.1	|- ( ph -> A e. V )
2		unexd.2	|- ( ph -> B e. W )
3		unexg	|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
4	1 2 3	syl2anc	|- ( ph -> ( A u. B ) e. _V )