Metamath Proof Explorer

Theorem dmxpid

Description: The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995)

Ref Expression
Assertion dmxpid 
|- dom ( A X. A ) = A

Proof

Step Hyp Ref Expression
1 dm0 
 |-  dom (/) = (/)
2 xpeq1 
 |-  ( A = (/) -> ( A X. A ) = ( (/) X. A ) )
3 0xp 
 |-  ( (/) X. A ) = (/)
4 2 3 eqtrdi 
 |-  ( A = (/) -> ( A X. A ) = (/) )
5 4 dmeqd 
 |-  ( A = (/) -> dom ( A X. A ) = dom (/) )
6 id 
 |-  ( A = (/) -> A = (/) )
7 1 5 6 3eqtr4a 
 |-  ( A = (/) -> dom ( A X. A ) = A )
8 dmxp 
 |-  ( A =/= (/) -> dom ( A X. A ) = A )
9 7 8 pm2.61ine 
 |-  dom ( A X. A ) = A