Metamath Proof Explorer


Theorem rnxpid

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

Ref Expression
Assertion rnxpid
|- ran ( A X. A ) = A

Proof

Step Hyp Ref Expression
1 rn0
 |-  ran (/) = (/)
2 xpeq2
 |-  ( A = (/) -> ( A X. A ) = ( A X. (/) ) )
3 xp0
 |-  ( A X. (/) ) = (/)
4 2 3 eqtrdi
 |-  ( A = (/) -> ( A X. A ) = (/) )
5 4 rneqd
 |-  ( A = (/) -> ran ( A X. A ) = ran (/) )
6 id
 |-  ( A = (/) -> A = (/) )
7 1 5 6 3eqtr4a
 |-  ( A = (/) -> ran ( A X. A ) = A )
8 rnxp
 |-  ( A =/= (/) -> ran ( A X. A ) = A )
9 7 8 pm2.61ine
 |-  ran ( A X. A ) = A