Metamath Proof Explorer


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 × A = B × B A = B

Proof

Step Hyp Ref Expression
1 dmeq A × A = B × B dom A × A = dom B × B
2 dmxpid dom A × A = A
3 dmxpid dom B × B = B
4 1 2 3 3eqtr3g A × A = B × B A = B
5 xpeq12 A = B A = B A × A = B × B
6 5 anidms A = B A × A = B × B
7 4 6 impbii A × A = B × B A = B