Theorem xpex

Description: The Cartesian product of two sets is a set. Proposition 6.2 of TakeutiZaring p. 23. (Contributed by NM, 14-Aug-1994)

	Ref	Expression
Hypotheses	xpex.1	$$⊢A\in \mathrm{V}$$
	xpex.2	$$⊢B\in \mathrm{V}$$
Assertion	xpex	$$⊢A\times B\in \mathrm{V}$$

Proof

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