Theorem rnxpid

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

	Ref	Expression
Assertion	rnxpid	⊢ ran ( 𝐴 × 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		rn0	⊢ ran ∅ = ∅
2		xpeq2	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ( 𝐴 × ∅ ) )
3		xp0	⊢ ( 𝐴 × ∅ ) = ∅
4	2 3	eqtrdi	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ∅ )
5	4	rneqd	⊢ ( 𝐴 = ∅ → ran ( 𝐴 × 𝐴 ) = ran ∅ )
6		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
7	1 5 6	3eqtr4a	⊢ ( 𝐴 = ∅ → ran ( 𝐴 × 𝐴 ) = 𝐴 )
8		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐴 ) = 𝐴 )
9	7 8	pm2.61ine	⊢ ran ( 𝐴 × 𝐴 ) = 𝐴