rnxpid

Description: The range of a Cartesian square. (Contributed by FL, 17-May-2010)

		Ref	Expression
	Assertion	rnxpid	$⊢ ran (A \times A) = A$

Step	Hyp	Ref	Expression
1		rn0	$⊢ ran \emptyset = \emptyset$
2		xpeq2	$⊢ A = \emptyset \to A \times A = A \times \emptyset$
3		xp0	$⊢ A \times \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ A = \emptyset \to A \times A = \emptyset$
5	4	rneqd	$⊢ A = \emptyset \to ran (A \times A) = ran \emptyset$
6		id	$⊢ A = \emptyset \to A = \emptyset$
7	1 5 6	3eqtr4a	$⊢ A = \emptyset \to ran (A \times A) = A$
8		rnxp	$⊢ A \neq \emptyset \to ran (A \times A) = A$
9	7 8	pm2.61ine	$⊢ ran (A \times A) = A$

Metamath Proof Explorer