Theorem inv_img_dist_union

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

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