Theorem unexd

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

	Ref	Expression
Hypotheses	unexd.1	$$⊢\phi \to A\in V$$
	unexd.2	$$⊢\phi \to B\in W$$
Assertion	unexd	$$⊢\phi \to A\cup B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		unexd.1	$$⊢\phi \to A\in V$$
2		unexd.2	$$⊢\phi \to B\in W$$
3		unexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\cup B\in \mathrm{V}$$
4	1 2 3	syl2anc	$$⊢\phi \to A\cup B\in \mathrm{V}$$