Theorem img_dist_union

Proof
01. 1 ⊢ y ∈ img R (A ∪ B), hypo.
02. 1 ⊢ ∃x. x ∈ A ∪ B ∧ (x, y) ∈ R, img_elim 1.
03. 3 ⊢ x ∈ A ∪ B ∧ (x, y) ∈ R, hypo.
04. 3 ⊢ (x, y) ∈ R, conj_elimr 3.
05. 3 ⊢ x ∈ A ∪ B, conj_eliml 3.
06. 3 ⊢ x ∈ A ∨ x ∈ B, union_elim 5.
07. 7 ⊢ x ∈ A, hypo.
08. 3, 7 ⊢ y ∈ img R A, img_intro 7 4.
09. 3, 7 ⊢ y ∈ img R A ∪ img R B, union_introl 8.
10. 10 ⊢ x ∈ B, hypo.
11. 3, 10 ⊢ y ∈ img R B, img_intro 10 4.
12. 3, 10 ⊢ y ∈ img R A ∪ img R B, union_intror 11.
13. 3 ⊢ y ∈ img R A ∪ img R B, disj_elim 6 9 12.
14. 1 ⊢ y ∈ img R A ∪ img R B, ex_elim 2 13.
15. ⊢ y ∈ img R (A ∪ B) → y ∈ img R A ∪ img R B, subj_intro 14.
16. 16 ⊢ y ∈ img R A ∪ img R B, hypo.
17. 16 ⊢ y ∈ img R A ∨ y ∈ img R B, union_elim 16.
18. 18 ⊢ y ∈ img R A, hypo.
19. 18 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ R, img_elim 18.
20. 20 ⊢ x ∈ A ∧ (x, y) ∈ R, hypo.
21. 20 ⊢ x ∈ A, conj_eliml 20.
22. 20 ⊢ (x, y) ∈ R, conj_elimr 20.
23. 20 ⊢ x ∈ A ∪ B, union_introl 21.
24. 20 ⊢ y ∈ img R (A ∪ B), img_intro 23 22.
25. 18 ⊢ y ∈ img R (A ∪ B), ex_elim 19 24.
26. 26 ⊢ y ∈ img R B, hypo.
27. 26 ⊢ ∃x. x ∈ B ∧ (x, y) ∈ R, img_elim 26.
28. 28 ⊢ x ∈ B ∧ (x, y) ∈ R, hypo.
29. 28 ⊢ x ∈ B, conj_eliml 28.
30. 28 ⊢ (x, y) ∈ R, conj_elimr 28.
31. 28 ⊢ x ∈ A ∪ B, union_intror 29.
32. 28 ⊢ y ∈ img R (A ∪ B), img_intro 31 30.
33. 26 ⊢ y ∈ img R (A ∪ B), ex_elim 27 32.
34. 16 ⊢ y ∈ img R (A ∪ B), disj_elim 17 25 33.
35. ⊢ y ∈ img R A ∪ img R B → y ∈ img R (A ∪ B), subj_intro 34.
36. ⊢ y ∈ img R (A ∪ B) ↔ y ∈ img R A ∪ img R B, bij_intro 15 35.
37. ⊢ ∀y. y ∈ img R (A ∪ B) ↔ y ∈ img R A ∪ img R B, uq_intro 36.
img_dist_union. ⊢ img R (A ∪ B) = img R A ∪ img R B, ext 37.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.