Metamath Proof Explorer


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 ( 𝐴 × 𝐴 ) = 𝐴