Theorem xpexd

Description: The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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