Theorem app_elim_lemma

Proof
01. 1 ⊢ ∃y. set y ∧ {y} = {y | (x, y) ∈ f}, hypo.
02. 2 ⊢ y = app f x, hypo.
03. 2 ⊢ y = ⋂{y | (x, y) ∈ f}, eq_subst app_eq 2, P u ↔ y = u.
04. 4 ⊢ set b ∧ {b} = {y | (x, y) ∈ f}, hypo.
05. 4 ⊢ set b, conj_eliml 4.
06. 4 ⊢ {b} = {y | (x, y) ∈ f}, conj_elimr 4.
07. 2, 4 ⊢ y = ⋂{b}, eq_subst_rev 6 3, P u ↔ y = ⋂u.
08. 4 ⊢ ⋂{b} = b, Intersection_sg 5.
09. 2, 4 ⊢ y = b, eq_trans 7 8.
10. 2, 4 ⊢ y ∈ {b}, sg_intro 5 9.
11. 2, 4 ⊢ y ∈ {y | (x, y) ∈ f}, eq_subst 6 10, P u ↔ y ∈ u.
12. 2, 4 ⊢ (x, y) ∈ f, comp_elim 11.
13. 1, 2 ⊢ (x, y) ∈ f, ex_elim 1 12.
app_elim_lemma. ⊢ (∃y. set y ∧ {y} = {y | (x, y) ∈ f}) →
  y = app f x → (x, y) ∈ f, subj_intro_ii 13.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.