Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ x ∈ dom f, hypo.
03. 3 ⊢ y = app f x, hypo.
04. 3 ⊢ y = ⋂{y | (x, y) ∈ f}, eq_subst app_eq 3, P u ↔ y = u.
05. 1, 2 ⊢ ∃y. set y ∧ {y} = {y | (x, y) ∈ f}, fn_img_lemma 1 2.
06. 6 ⊢ set b ∧ {b} = {y | (x, y) ∈ f}, hypo.
07. 6 ⊢ set b, conj_eliml 6.
08. 6 ⊢ {b} = {y | (x, y) ∈ f}, conj_elimr 6.
09. 3, 6 ⊢ y = ⋂{b}, eq_subst_rev 8 4, P u ↔ y = ⋂u.
10. 6 ⊢ ⋂{b} = b, Intersection_sg 7.
11. 3, 6 ⊢ y = b, eq_trans 9 10.
12. 3, 6 ⊢ y ∈ {b}, sg_intro 7 11.
13. 3, 6 ⊢ y ∈ {y | (x, y) ∈ f}, eq_subst 8 12, P u ↔ y ∈ u.
14. 3, 6 ⊢ (x, y) ∈ f, comp_elim 13.
15. 1, 2, 3 ⊢ (x, y) ∈ f, ex_elim 5 14.
app_elim. ⊢ function f → x ∈ dom f → y = app f x → (x, y) ∈ f,
subj_intro_iii 15.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.