This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 B ∪ C = A B ∪ A C

Proof

Step Hyp Ref Expression
1 resundi ⊢ A ↾ B ∪ C = A ↾ B ∪ A ↾ C
2 1 rneqi ⊢ ran ⁡ A ↾ B ∪ C = ran ⁡ A ↾ B ∪ A ↾ C
3 rnun ⊢ ran ⁡ A ↾ B ∪ A ↾ C = ran ⁡ A ↾ B ∪ ran ⁡ A ↾ C
4 2 3 eqtri ⊢ ran ⁡ A ↾ B ∪ C = ran ⁡ A ↾ B ∪ ran ⁡ A ↾ C
5 df-ima ⊢ A B ∪ C = ran ⁡ A ↾ B ∪ C
6 df-ima ⊢ A B = ran ⁡ A ↾ B
7 df-ima ⊢ A C = ran ⁡ A ↾ C
8 6 7 uneq12i ⊢ A B ∪ A C = ran ⁡ A ↾ B ∪ ran ⁡ A ↾ C
9 4 5 8 3eqtr4i ⊢ A B ∪ C = A B ∪ A C