Theorem imaundi 6011

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 5870	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5810	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6007	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2847	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5571	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5571	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5571	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4140	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2857	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1536   ∪ cun 3937  ran crn 5559   ↾ cres 5560   “ cima 5561

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-xp 5564  df-cnv 5566  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571

This theorem is referenced by:  fnimapr  6750  domunfican  8794  fiint  8798  fodomfi  8800  marypha1lem  8900  resunimafz0  13806  dprd2da  19167  dmdprdsplit2lem  19170  uniioombllem3  24189  mbfimaicc  24235  plyeq0  24804  fnimatp  30426  ffsrn  30468  tocyccntz  30790  noetalem4  33224  imadifss  34871  poimirlem1  34897  poimirlem2  34898  poimirlem3  34899  poimirlem4  34900  poimirlem6  34902  poimirlem7  34903  poimirlem11  34907  poimirlem12  34908  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem19  34915  poimirlem20  34916  poimirlem23  34919  poimirlem24  34920  poimirlem25  34921  poimirlem29  34925  poimirlem31  34927  mbfposadd  34943  itg2addnclem2  34948  ftc1anclem1  34971  ftc1anclem5  34975  brtrclfv2  40078  frege77d  40097  frege109d  40108  frege131d  40115  dffrege76  40291  icccncfext  42176