Metamath Proof Explorer

Theorem rnxp

Description: The range of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004)

Ref Expression
Assertion rnxp 
|- ( A =/= (/) -> ran ( A X. B ) = B )

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran ( A X. B ) = dom `' ( A X. B )
2 cnvxp 
 |-  `' ( A X. B ) = ( B X. A )
3 2 dmeqi 
 |-  dom `' ( A X. B ) = dom ( B X. A )
4 1 3 eqtri 
 |-  ran ( A X. B ) = dom ( B X. A )
5 dmxp 
 |-  ( A =/= (/) -> dom ( B X. A ) = B )
6 4 5 syl5eq 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )