dmxpid

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

		Ref	Expression
	Assertion	dmxpid	$⊢ dom (A \times A) = A$

Step	Hyp	Ref	Expression
1		dm0	$⊢ dom \emptyset = \emptyset$
2		xpeq1	$⊢ A = \emptyset \to A \times A = \emptyset \times A$
3		0xp	$⊢ \emptyset \times A = \emptyset$
4	2 3	eqtrdi	$⊢ A = \emptyset \to A \times A = \emptyset$
5	4	dmeqd	$⊢ A = \emptyset \to dom (A \times A) = dom \emptyset$
6		id	$⊢ A = \emptyset \to A = \emptyset$
7	1 5 6	3eqtr4a	$⊢ A = \emptyset \to dom (A \times A) = A$
8		dmxp	$⊢ A \neq \emptyset \to dom (A \times A) = A$
9	7 8	pm2.61ine	$⊢ dom (A \times A) = A$

Metamath Proof Explorer