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	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	sqxpeqd	⊢ ( 𝜑 → ( 𝐴 × 𝐴 ) = ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2	1 1	xpeq12d	⊢ ( 𝜑 → ( 𝐴 × 𝐴 ) = ( 𝐵 × 𝐵 ) )