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