Theorem imaundi 6102

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 5948	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5883	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6098	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2752	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5636	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5636	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5636	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4119	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2762	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1540   ∪ cun 3903  ran crn 5624   ↾ cres 5625   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  cnvimassrndm  6105  fnimapr  6910  fnimatpd  6911  naddasslem1  8619  naddasslem2  8620  fodomfi  9219  imafiOLD  9223  domunfican  9230  fiint  9235  fiintOLD  9236  fodomfiOLD  9239  marypha1lem  9342  resunimafz0  14370  dprd2da  19941  dmdprdsplit2lem  19944  uniioombllem3  25502  mbfimaicc  25548  plyeq0  26132  madeoldsuc  27817  addsbday  27947  negsbdaylem  27985  zs12bday  28379  ffsrn  32685  tocyccntz  33099  imadifss  37577  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem11  37613  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem29  37631  poimirlem31  37633  mbfposadd  37649  itg2addnclem2  37654  ftc1anclem1  37675  ftc1anclem5  37679  brtrclfv2  43703  frege77d  43722  frege109d  43733  frege131d  43740  dffrege76  43915  icccncfext  45872  cycl3grtri  47935