Metamath Proof Explorer

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 ∪ B = ran ⁡ F ↾ A ∪ ran ⁡ F ↾ B

Proof

Step Hyp Ref Expression
1 resundi ⊢ F ↾ A ∪ B = F ↾ A ∪ F ↾ B
2 1 rneqi ⊢ ran ⁡ F ↾ A ∪ B = ran ⁡ F ↾ A ∪ F ↾ B
3 rnun ⊢ ran ⁡ F ↾ A ∪ F ↾ B = ran ⁡ F ↾ A ∪ ran ⁡ F ↾ B
4 2 3 eqtri ⊢ ran ⁡ F ↾ A ∪ B = ran ⁡ F ↾ A ∪ ran ⁡ F ↾ B