Theorem rnresun

Description: Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	rnresun	|- ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )

Proof

Step	Hyp	Ref	Expression
1		resundi	|- ( F |` ( A u. B ) ) = ( ( F |` A ) u. ( F |` B ) )
2	1	rneqi	|- ran ( F |` ( A u. B ) ) = ran ( ( F |` A ) u. ( F |` B ) )
3		rnun	|- ran ( ( F |` A ) u. ( F |` B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )
4	2 3	eqtri	|- ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )