Theorem imaundi 6053

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 5905	. . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
2	1	rneqi 5846	. . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))
3		rnun 6049	. . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
4	2, 3	eqtri 2766	. 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
5		df-ima 5602	. 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶))
6		df-ima 5602	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
7		df-ima 5602	. . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
8	6, 7	uneq12i 4095	. 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶))
9	4, 5, 8	3eqtr4i 2776	1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶))

Syntax hints:   = wceq 1539   ∪ cun 3885  ran crn 5590   ↾ cres 5591   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  cnvimassrndm  6055  fnimapr  6852  imafi  8958  domunfican  9087  fiint  9091  fodomfi  9092  marypha1lem  9192  resunimafz0  14157  dprd2da  19645  dmdprdsplit2lem  19648  uniioombllem3  24749  mbfimaicc  24795  plyeq0  25372  fnimatp  31014  ffsrn  31064  tocyccntz  31411  madeoldsuc  34067  imadifss  35752  poimirlem1  35778  poimirlem2  35779  poimirlem3  35780  poimirlem4  35781  poimirlem6  35783  poimirlem7  35784  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem23  35800  poimirlem24  35801  poimirlem25  35802  poimirlem29  35806  poimirlem31  35808  mbfposadd  35824  itg2addnclem2  35829  ftc1anclem1  35850  ftc1anclem5  35854  brtrclfv2  41335  frege77d  41354  frege109d  41365  frege131d  41372  dffrege76  41547  icccncfext  43428