map_app_is

Theorem map_app_is_set

Theorem. map_app_is_set
map f X Y → x ∈ X → set (app f x)

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 1, 2 ⊢ app f x ∈ Y, map_app_in_cod 1 2.
04. 1, 2 ⊢ set (app f x), set_intro 3.
map_app_is_set. ⊢ map f X Y → x ∈ X → set (app f x), subj_intro_ii 4.

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