Theorem rnxpid

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

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

Proof

Step	Hyp	Ref	Expression
1		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
2		xpeq2	$$⊢A=\varnothing \to A\times A=A\times \varnothing$$
3		xp0	$$⊢A\times \varnothing =\varnothing$$
4	2 3	eqtrdi	$$⊢A=\varnothing \to A\times A=\varnothing$$
5	4	rneqd	$$⊢A=\varnothing \to \mathrm{ran}\left(A\times A\right)=\mathrm{ran}\varnothing$$
6		id	$$⊢A=\varnothing \to A=\varnothing$$
7	1 5 6	3eqtr4a	$$⊢A=\varnothing \to \mathrm{ran}\left(A\times A\right)=A$$
8		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times A\right)=A$$
9	7 8	pm2.61ine	$$⊢\mathrm{ran}\left(A\times A\right)=A$$