Theorem dmxpid

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

	Ref	Expression
Assertion	dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
2		xpeq1	$$⊢A=\varnothing \to A\times A=\varnothing \times A$$
3		0xp	$$⊢\varnothing \times A=\varnothing$$
4	2 3	syl6eq	$$⊢A=\varnothing \to A\times A=\varnothing$$
5	4	dmeqd	$$⊢A=\varnothing \to \mathrm{dom}\left(A\times A\right)=\mathrm{dom}\varnothing$$
6		id	$$⊢A=\varnothing \to A=\varnothing$$
7	1 5 6	3eqtr4a	$$⊢A=\varnothing \to \mathrm{dom}\left(A\times A\right)=A$$
8		dmxp	$$⊢A\ne \varnothing \to \mathrm{dom}\left(A\times A\right)=A$$
9	7 8	pm2.61ine	$$⊢\mathrm{dom}\left(A\times A\right)=A$$