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 X. A ) = ( B X. B ) <-> A = B )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( ( A X. A ) = ( B X. B ) -> dom ( A X. A ) = dom ( B X. B ) )
2 dmxpid 
 |-  dom ( A X. A ) = A
3 dmxpid 
 |-  dom ( B X. B ) = B
4 1 2 3 3eqtr3g 
 |-  ( ( A X. A ) = ( B X. B ) -> A = B )
5 xpeq12 
 |-  ( ( A = B /\ A = B ) -> ( A X. A ) = ( B X. B ) )
6 5 anidms 
 |-  ( A = B -> ( A X. A ) = ( B X. B ) )
7 4 6 impbii 
 |-  ( ( A X. A ) = ( B X. B ) <-> A = B )