Theorem imaundi 6091

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 5937	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5872	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6087	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2754	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5624	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5624	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5624	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4111	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2764	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1541   ∪ cun 3895  ran crn 5612   ↾ cres 5613   “ cima 5614

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703

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-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-cnv 5619  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624

This theorem is referenced by:  cnvimassrndm  6094  fnimapr  6900  fnimatpd  6901  naddasslem1  8604  naddasslem2  8605  fodomfi  9191  imafiOLD  9195  domunfican  9201  fiint  9206  fodomfiOLD  9209  marypha1lem  9312  resunimafz0  14347  dprd2da  19951  dmdprdsplit2lem  19954  uniioombllem3  25508  mbfimaicc  25554  plyeq0  26138  madeoldsuc  27825  addsbday  27955  negsbdaylem  27993  zs12bday  28389  ffsrn  32703  tocyccntz  33105  imadifss  37635  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem11  37671  poimirlem12  37672  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem29  37689  poimirlem31  37691  mbfposadd  37707  itg2addnclem2  37712  ftc1anclem1  37733  ftc1anclem5  37737  brtrclfv2  43760  frege77d  43779  frege109d  43790  frege131d  43797  dffrege76  43972  icccncfext  45925  cycl3grtri  47978