Theorem 3xpexg

Description: The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018)

	Ref	Expression
Assertion	3xpexg	$$⊢V\in W\to \left(V\times V\right)\times V\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		xpexg	$$⊢\left(V\in W\wedge V\in W\right)\to V\times V\in \mathrm{V}$$
2	1	anidms	$$⊢V\in W\to V\times V\in \mathrm{V}$$
3		xpexg	$$⊢\left(V\times V\in \mathrm{V}\wedge V\in W\right)\to \left(V\times V\right)\times V\in \mathrm{V}$$
4	2 3	mpancom	$$⊢V\in W\to \left(V\times V\right)\times V\in \mathrm{V}$$