Theorem imaundi 6107

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

Assertion

Ref	Expression
imaundi	⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Proof of Theorem imaundi

Step	Hyp	Ref	Expression
1		resundi 5952	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5886	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6103	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2759	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5637	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5637	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5637	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4118	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2769	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1541   ∪ cun 3899  ran crn 5625   ↾ cres 5626   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  cnvimassrndm  6110  fnimapr  6917  fnimatpd  6918  naddasslem1  8622  naddasslem2  8623  fodomfi  9212  imafiOLD  9216  domunfican  9222  fiint  9227  fodomfiOLD  9230  marypha1lem  9336  resunimafz0  14368  dprd2da  19973  dmdprdsplit2lem  19976  uniioombllem3  25542  mbfimaicc  25588  plyeq0  26172  madeoldsuc  27881  addbday  28014  negbdaylem  28052  bdaypw2n0bndlem  28459  ffsrn  32807  tocyccntz  33226  imadifss  37796  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  mbfposadd  37868  itg2addnclem2  37873  ftc1anclem1  37894  ftc1anclem5  37898  brtrclfv2  43968  frege77d  43987  frege109d  43998  frege131d  44005  dffrege76  44180  icccncfext  46131  cycl3grtri  48193