Theorem bnj1149

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

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