Theorem imaundi 6104

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 5949	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5884	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6100	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2756	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5634	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5634	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5634	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4117	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2766	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1541   ∪ cun 3897  ran crn 5622   ↾ cres 5623   “ cima 5624

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  cnvimassrndm  6107  fnimapr  6914  fnimatpd  6915  naddasslem1  8618  naddasslem2  8619  fodomfi  9206  imafiOLD  9210  domunfican  9216  fiint  9221  fodomfiOLD  9224  marypha1lem  9327  resunimafz0  14362  dprd2da  19966  dmdprdsplit2lem  19969  uniioombllem3  25523  mbfimaicc  25569  plyeq0  26153  madeoldsuc  27840  addsbday  27970  negsbdaylem  28008  zs12bday  28404  ffsrn  32722  tocyccntz  33124  imadifss  37645  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem11  37681  poimirlem12  37682  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem29  37699  poimirlem31  37701  mbfposadd  37717  itg2addnclem2  37722  ftc1anclem1  37743  ftc1anclem5  37747  brtrclfv2  43834  frege77d  43853  frege109d  43864  frege131d  43871  dffrege76  44046  icccncfext  45999  cycl3grtri  48061