Theorem sqxpeqd

Description: Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power . (Contributed by AV, 13-Jan-2020)

	Ref	Expression
Hypothesis	xpeq1d.1	$$⊢\phi \to A=B$$
Assertion	sqxpeqd	$$⊢\phi \to A\times A=B\times B$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1d.1	$$⊢\phi \to A=B$$
2	1 1	xpeq12d	$$⊢\phi \to A\times A=B\times B$$