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 ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		resundi	⊢ ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ 𝐵 ) )
2	1	rneqi	⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ 𝐵 ) )
3		rnun	⊢ ran ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐹 ↾ 𝐵 ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) )
4	2 3	eqtri	⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) )