# Metamath Proof Explorer

## Theorem imaundi

Description: Distributive law for image over union. Theorem 35 of Suppes p. 65. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion imaundi ${⊢}{A}\left[{B}\cup {C}\right]={A}\left[{B}\right]\cup {A}\left[{C}\right]$

### Proof

Step Hyp Ref Expression
1 resundi ${⊢}{{A}↾}_{\left({B}\cup {C}\right)}=\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)$
2 1 rneqi ${⊢}\mathrm{ran}\left({{A}↾}_{\left({B}\cup {C}\right)}\right)=\mathrm{ran}\left(\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)\right)$
3 rnun ${⊢}\mathrm{ran}\left(\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)\right)=\mathrm{ran}\left({{A}↾}_{{B}}\right)\cup \mathrm{ran}\left({{A}↾}_{{C}}\right)$
4 2 3 eqtri ${⊢}\mathrm{ran}\left({{A}↾}_{\left({B}\cup {C}\right)}\right)=\mathrm{ran}\left({{A}↾}_{{B}}\right)\cup \mathrm{ran}\left({{A}↾}_{{C}}\right)$
5 df-ima ${⊢}{A}\left[{B}\cup {C}\right]=\mathrm{ran}\left({{A}↾}_{\left({B}\cup {C}\right)}\right)$
6 df-ima ${⊢}{A}\left[{B}\right]=\mathrm{ran}\left({{A}↾}_{{B}}\right)$
7 df-ima ${⊢}{A}\left[{C}\right]=\mathrm{ran}\left({{A}↾}_{{C}}\right)$
8 6 7 uneq12i ${⊢}{A}\left[{B}\right]\cup {A}\left[{C}\right]=\mathrm{ran}\left({{A}↾}_{{B}}\right)\cup \mathrm{ran}\left({{A}↾}_{{C}}\right)$
9 4 5 8 3eqtr4i ${⊢}{A}\left[{B}\cup {C}\right]={A}\left[{B}\right]\cup {A}\left[{C}\right]$