Metamath Proof Explorer
Description: The Cartesian square of a set is a set. (Contributed by AV, 13Jan2020)


Ref 
Expression 

Assertion 
sqxpexg 
$${\u22a2}{A}\in {V}\to {A}\times {A}\in \mathrm{V}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

xpexg 
$${\u22a2}\left({A}\in {V}\wedge {A}\in {V}\right)\to {A}\times {A}\in \mathrm{V}$$ 
2 
1

anidms 
$${\u22a2}{A}\in {V}\to {A}\times {A}\in \mathrm{V}$$ 