Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ x ∈ dom f, hypo.
03. 2 ⊢ ∃y. (x, y) ∈ f, dom_elim 2.
04. 4 ⊢ (x, y) ∈ f, hypo.
05. 5 ⊢ u ∈ {y}, hypo.
06. 4 ⊢ set (x, y), set_intro 4.
07. 4 ⊢ set y, setr_from_pair 6.
08. 4, 5 ⊢ u = y, sg_elim 7 5.
09. 4, 5 ⊢ set u, eq_subst_rev 8 7.
10. 4, 5 ⊢ (x, u) ∈ f, eq_subst_rev 8 4.
11. 4, 5 ⊢ u ∈ {y | (x, y) ∈ f}, comp_intro 9 10.
12. 4 ⊢ u ∈ {y} → u ∈ {y | (x, y) ∈ f}, subj_intro 11.
13. 13 ⊢ u ∈ {y | (x, y) ∈ f}, hypo.
14. 13 ⊢ (x, u) ∈ f, comp_elim 13.
15. 1, 4, 13 ⊢ u = y, fn_unique_value 1 14 4.
16. 13 ⊢ set u, set_intro 13.
17. 1, 4, 13 ⊢ set y, eq_subst 15 16.
18. 1, 4, 13 ⊢ u ∈ {y}, sg_intro 17 15.
19. 1, 4 ⊢ u ∈ {y | (x, y) ∈ f} → u ∈ {y}, subj_intro 18.
20. 1, 4 ⊢ u ∈ {y} ↔ u ∈ {y | (x, y) ∈ f}, bij_intro 12 19.
21. 1, 4 ⊢ ∀u. u ∈ {y} ↔ u ∈ {y | (x, y) ∈ f}, uq_intro 20.
22. 1, 4 ⊢ {y} = {y | (x, y) ∈ f}, ext 21.
23. 1, 4 ⊢ set y ∧ {y} = {y | (x, y) ∈ f}, conj_intro 7 22.
24. 1, 4 ⊢ ∃y. set y ∧ {y} = {y | (x, y) ∈ f}, ex_intro 23.
25. 1, 2 ⊢ ∃y. set y ∧ {y} = {y | (x, y) ∈ f}, ex_elim 3 24.
fn_img_lemma. ⊢ function f → x ∈ dom f →
∃y. set y ∧ {y} = {y | (x, y) ∈ f}, subj_intro_ii 25.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.