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