map_img_of_dom_is

Theorem map_img_of_dom_is_rng

Theorem. map_img_of_dom_is_rng
map f X Y → img f X = rng f

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ dom f = X, map_dom 1.
03. ⊢ img f (dom f) = rng f, img_of_dom_is_rng.
04. 1 ⊢ img f X = rng f, eq_subst 2 3, P t ↔ img f t = rng f.
map_img_of_dom_is_rng. ⊢ map f X Y → img f X = rng f, subj_intro 4.

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