Theorem imaundi 6140

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 5983	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5918	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6135	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2783	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5663	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5663	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5663	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4165	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2793	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4149  ran crn 5651   ↾ cres 5652   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  cnvimassrndmOLD  6199  imadifssrn  6201  fnimapr  6969  fnimatpd  6970  naddasslem1  8708  naddasslem2  8709  fodomfi  9308  domunfican  9317  fiint  9322  marypha1lem  9429  resunimafz0  14594  dprd2da  20264  dmdprdsplit2lem  20267  uniioombllem3  25912  mbfimaicc  25958  plyeq0  26536  madeoldsuc  28277  addbday  28410  negbdaylem  28448  bdaypw2n0bndlem  28855  ffsrn  33367  tocyccntz  33752  imadifss  38617  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem11  38643  poimirlem12  38644  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem29  38661  poimirlem31  38663  mbfposadd  38679  itg2addnclem2  38684  ftc1anclem1  38705  ftc1anclem5  38709  brtrclfv2  44821  frege77d  44840  frege109d  44851  frege131d  44858  dffrege76  45033  icccncfext  46991  cycl3grtri  49139