Theorem xpid11

Description: The Cartesian square is a one-to-one construction. (Contributed by NM, 5-Nov-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	xpid11	$$⊢A\times A=B\times B\leftrightarrow A=B$$

Proof

Step	Hyp	Ref	Expression
1		dmeq	$$⊢A\times A=B\times B\to \mathrm{dom}\left(A\times A\right)=\mathrm{dom}\left(B\times B\right)$$
2		dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$
3		dmxpid	$$⊢\mathrm{dom}\left(B\times B\right)=B$$
4	1 2 3	3eqtr3g	$$⊢A\times A=B\times B\to A=B$$
5		xpeq12	$$⊢\left(A=B\wedge A=B\right)\to A\times A=B\times B$$
6	5	anidms	$$⊢A=B\to A\times A=B\times B$$
7	4 6	impbii	$$⊢A\times A=B\times B\leftrightarrow A=B$$