Theorem imaundi 5408

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

Assertion

Ref	Expression
imaundi	|- ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )

Proof of Theorem imaundi

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

Syntax hints:   = wceq 1383   u. cun 3459   ran crn 4990   |` cres 4991   "cima 4992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002

This theorem is referenced by:  fnimapr  5922  domunfican  7795  fiint  7799  fodomfi  7801  marypha1lem  7895  dprd2da  17070  dmdprdsplit2lem  17073  uniioombllem3  21972  mbfimaicc  22018  plyeq0  22586  eupath2lem3  24957  ffsrn  27530  mbfposadd  30038  itg2addnclem2  30043  ftc1anclem1  30066  ftc1anclem5  30070  icccncfext  31644