Theorem rnun

Description: Distributive law for range over union. Theorem 8 of Suppes p. 60. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	rnun	|- ran ( A u. B ) = ( ran A u. ran B )

Proof

Step	Hyp	Ref	Expression
1		cnvun	|- `' ( A u. B ) = ( `' A u. `' B )
2	1	dmeqi	|- dom `' ( A u. B ) = dom ( `' A u. `' B )
3		dmun	|- dom ( `' A u. `' B ) = ( dom `' A u. dom `' B )
4	2 3	eqtri	|- dom `' ( A u. B ) = ( dom `' A u. dom `' B )
5		df-rn	|- ran ( A u. B ) = dom `' ( A u. B )
6		df-rn	|- ran A = dom `' A
7		df-rn	|- ran B = dom `' B
8	6 7	uneq12i	|- ( ran A u. ran B ) = ( dom `' A u. dom `' B )
9	4 5 8	3eqtr4i	|- ran ( A u. B ) = ( ran A u. ran B )