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 u. C ) ) = ( ( A " B ) u. ( A " C ) )

Proof

Step Hyp Ref Expression
1 resundi 
 |-  ( A |` ( B u. C ) ) = ( ( A |` B ) u. ( A |` C ) )
2 1 rneqi 
 |-  ran ( A |` ( B u. C ) ) = ran ( ( A |` B ) u. ( A |` C ) )
3 rnun 
 |-  ran ( ( A |` B ) u. ( A |` C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
4 2 3 eqtri 
 |-  ran ( A |` ( B u. C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
5 df-ima 
 |-  ( A " ( B u. C ) ) = ran ( A |` ( B u. C ) )
6 df-ima 
 |-  ( A " B ) = ran ( A |` B )
7 df-ima 
 |-  ( A " C ) = ran ( A |` C )
8 6 7 uneq12i 
 |-  ( ( A " B ) u. ( A " C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
9 4 5 8 3eqtr4i 
 |-  ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )