Theorem imaundi 5254

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 5124	. . . 4 |- ( A |` ( B u. C ) ) = ( ( A |` B ) u. ( A |` C ) )
2	1	rneqi 5067	. . 3 |- ran ( A |` ( B u. C ) ) = ran ( ( A |` B ) u. ( A |` C ) )
3		rnun 5250	. . 3 |- ran ( ( A |` B ) u. ( A |` C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
4	2, 3	eqtri 2493	. 2 |- ran ( A |` ( B u. C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
5		df-ima 4852	. 2 |- ( A " ( B u. C ) ) = ran ( A |` ( B u. C ) )
6		df-ima 4852	. . 3 |- ( A " B ) = ran ( A |` B )
7		df-ima 4852	. . 3 |- ( A " C ) = ran ( A |` C )
8	6, 7	uneq12i 3577	. 2 |- ( ( A " B ) u. ( A " C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
9	4, 5, 8	3eqtr4i 2503	1 |- ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )

Syntax hints:   = wceq 1452   u. cun 3388   ran crn 4840   |` cres 4841   "cima 4842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-xp 4845  df-cnv 4847  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852

This theorem is referenced by:  fnimapr  5944  domunfican  7862  fiint  7866  fodomfi  7868  marypha1lem  7965  dprd2da  17753  dmdprdsplit2lem  17756  uniioombllem3  22622  mbfimaicc  22668  plyeq0  23244  eupath2lem3  25786  ffsrn  28389  imadifss  31992  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem6  32010  poimirlem7  32011  poimirlem11  32015  poimirlem12  32016  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem29  32033  poimirlem31  32035  mbfposadd  32052  itg2addnclem2  32058  ftc1anclem1  32081  ftc1anclem5  32085  brtrclfv2  36390  frege77d  36409  frege109d  36420  frege131d  36427  dffrege76  36606  icccncfext  37862  resunimafz0  39216