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