Theorem img_of_dom_is_rng

Proof
01. 1 ⊢ relation R, hypo.
02. 2 ⊢ y ∈ rng R, hypo.
03. 2 ⊢ ∃x. (x, y) ∈ R, rng_elim 2.
04. 4 ⊢ (x, y) ∈ R, hypo.
05. 4 ⊢ x ∈ dom R, dom_intro 4.
06. 4 ⊢ y ∈ img R (dom R), img_intro 5 4.
07. 2 ⊢ y ∈ img R (dom R), ex_elim 3 6.
08. ⊢ y ∈ rng R → y ∈ img R (dom R), subj_intro 7.
09. ⊢ ∀y. y ∈ rng R → y ∈ img R (dom R), uq_intro 8.
10. ⊢ rng R ⊆ img R (dom R), incl_intro 9.
11. ⊢ img R (dom R) ⊆ rng R, img_incl_in_rng.
img_of_dom_is_rng. ⊢ img R (dom R) = rng R, incl_antisym 11 10.

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