Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ (x, y) ∈ f, hypo.
03. 2 ⊢ x ∈ dom f, dom_intro 2.
04. 1, 2 ⊢ ∃y. set y ∧ {y} = {y | (x, y) ∈ f}, fn_img_lemma 1 3.
05. 1, 2 ⊢ y = app f x, app_intro_lemma 4 2.
app_intro. ⊢ function f → (x, y) ∈ f → y = app f x, subj_intro_ii 5.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.