Theorem inv_img_dist_inter

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

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