Theorem sqxpexg

Description: The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020)

	Ref	Expression
Assertion	sqxpexg	$$⊢A\in V\to A\times A\in \mathrm{V}$$

Proof

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