Theorem img_dist_inter

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 ∈ A ∩ B, conj_eliml 3.
05. 3 ⊢ x ∈ A, intersection_eliml 4.
06. 3 ⊢ x ∈ B, intersection_elimr 4.
07. 3 ⊢ (x, y) ∈ R, conj_elimr 3.
08. 3 ⊢ y ∈ img R A, img_intro 5 7.
09. 3 ⊢ y ∈ img R B, img_intro 6 7.
10. 3 ⊢ y ∈ img R A ∩ img R B, intersection_intro 8 9.
11. 1 ⊢ y ∈ img R A ∩ img R B, ex_elim 2 10.
12. ⊢ y ∈ img R (A ∩ B) → y ∈ img R A ∩ img R B, subj_intro 11.
13. ⊢ ∀y. y ∈ img R (A ∩ B) → y ∈ img R A ∩ img R B, uq_intro 12.
img_dist_inter. ⊢ img R (A ∩ B) ⊆ img R A ∩ img R B, incl_intro 13.

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