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	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran ( 𝐴 × 𝐵 ) = dom ◡ ( 𝐴 × 𝐵 )
2		cnvxp	⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
3	2	dmeqi	⊢ dom ◡ ( 𝐴 × 𝐵 ) = dom ( 𝐵 × 𝐴 )
4	1 3	eqtri	⊢ ran ( 𝐴 × 𝐵 ) = dom ( 𝐵 × 𝐴 )
5		dmxp	⊢ ( 𝐴 ≠ ∅ → dom ( 𝐵 × 𝐴 ) = 𝐵 )
6	4 5	syl5eq	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )