Metamath Proof Explorer


Theorem dmxpid

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

Ref Expression
Assertion dmxpid dom A × A = A

Proof

Step Hyp Ref Expression
1 dm0 dom =
2 xpeq1 A = A × A = × A
3 0xp × A =
4 2 3 eqtrdi A = A × A =
5 4 dmeqd A = dom A × A = dom
6 id A = A =
7 1 5 6 3eqtr4a A = dom A × A = A
8 dmxp A dom A × A = A
9 7 8 pm2.61ine dom A × A = A