Theorem inv_img_incl_in_dom

Proof
01. 1 ⊢ x ∈ inv_img R B, hypo.
02. 1 ⊢ ∃y. y ∈ B ∧ (x, y) ∈ R, inv_img_elim 1.
03. 3 ⊢ y ∈ B ∧ (x, y) ∈ R, hypo.
04. 3 ⊢ (x, y) ∈ R, conj_elimr 3.
05. 3 ⊢ x ∈ dom R, dom_intro 4.
06. 1 ⊢ x ∈ dom R, ex_elim 2 5.
07. ⊢ x ∈ inv_img R B → x ∈ dom R, subj_intro 6.
08. ⊢ ∀x. x ∈ inv_img R B → x ∈ dom R, uq_intro 7.
inv_img_incl_in_dom. ⊢ inv_img R B ⊆ dom R, incl_intro 8.

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