# Metamath Proof Explorer

## 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 ${⊢}\mathrm{ran}\left({A}\cup {B}\right)=\mathrm{ran}{A}\cup \mathrm{ran}{B}$

### Proof

Step Hyp Ref Expression
1 cnvun ${⊢}{\left({A}\cup {B}\right)}^{-1}={{A}}^{-1}\cup {{B}}^{-1}$
2 1 dmeqi ${⊢}\mathrm{dom}{\left({A}\cup {B}\right)}^{-1}=\mathrm{dom}\left({{A}}^{-1}\cup {{B}}^{-1}\right)$
3 dmun ${⊢}\mathrm{dom}\left({{A}}^{-1}\cup {{B}}^{-1}\right)=\mathrm{dom}{{A}}^{-1}\cup \mathrm{dom}{{B}}^{-1}$
4 2 3 eqtri ${⊢}\mathrm{dom}{\left({A}\cup {B}\right)}^{-1}=\mathrm{dom}{{A}}^{-1}\cup \mathrm{dom}{{B}}^{-1}$
5 df-rn ${⊢}\mathrm{ran}\left({A}\cup {B}\right)=\mathrm{dom}{\left({A}\cup {B}\right)}^{-1}$
6 df-rn ${⊢}\mathrm{ran}{A}=\mathrm{dom}{{A}}^{-1}$
7 df-rn ${⊢}\mathrm{ran}{B}=\mathrm{dom}{{B}}^{-1}$
8 6 7 uneq12i ${⊢}\mathrm{ran}{A}\cup \mathrm{ran}{B}=\mathrm{dom}{{A}}^{-1}\cup \mathrm{dom}{{B}}^{-1}$
9 4 5 8 3eqtr4i ${⊢}\mathrm{ran}\left({A}\cup {B}\right)=\mathrm{ran}{A}\cup \mathrm{ran}{B}$