Theorem imaundi 5264

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 5134	. . . 4 |- ( A |` ( B u. C ) ) = ( ( A |` B ) u. ( A |` C ) )
2	1	rneqi 5077	. . 3 |- ran ( A |` ( B u. C ) ) = ran ( ( A |` B ) u. ( A |` C ) )
3		rnun 5260	. . 3 |- ran ( ( A |` B ) u. ( A |` C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
4	2, 3	eqtri 2451	. 2 |- ran ( A |` ( B u. C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
5		df-ima 4863	. 2 |- ( A " ( B u. C ) ) = ran ( A |` ( B u. C ) )
6		df-ima 4863	. . 3 |- ( A " B ) = ran ( A |` B )
7		df-ima 4863	. . 3 |- ( A " C ) = ran ( A |` C )
8	6, 7	uneq12i 3618	. 2 |- ( ( A " B ) u. ( A " C ) ) = ( ran ( A |` B ) u. ran ( A |` C ) )
9	4, 5, 8	3eqtr4i 2461	1 |- ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )

Syntax hints:   = wceq 1437   u. cun 3434   ran crn 4851   |` cres 4852   "cima 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-cnv 4858  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863

This theorem is referenced by:  fnimapr  5942  domunfican  7847  fiint  7851  fodomfi  7853  marypha1lem  7950  dprd2da  17663  dmdprdsplit2lem  17666  uniioombllem3  22530  mbfimaicc  22576  plyeq0  23152  eupath2lem3  25693  ffsrn  28308  imadifss  31842  poimirlem1  31855  poimirlem2  31856  poimirlem3  31857  poimirlem4  31858  poimirlem6  31860  poimirlem7  31861  poimirlem11  31865  poimirlem12  31866  poimirlem15  31869  poimirlem16  31870  poimirlem17  31871  poimirlem19  31873  poimirlem20  31874  poimirlem23  31877  poimirlem24  31878  poimirlem25  31879  poimirlem29  31883  poimirlem31  31885  mbfposadd  31902  itg2addnclem2  31908  ftc1anclem1  31931  ftc1anclem5  31935  brtrclfv2  36179  frege77d  36198  frege109d  36209  frege131d  36216  dffrege76  36393  icccncfext  37585