Proof
01. 1 ⊢ fn_on f A, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 3 ⊢ y = app f x, hypo.
04. 1 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, ex_uniq_from_fn_on 1.
05. 1, 2 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_bounded_elim 4 2.
06. 1, 2 ⊢ ∃z. set z ∧ {z} = {y | (x, y) ∈ f}, sg_eq_from_ex_uniq 5.
07. 1, 2, 3 ⊢ (x, y) ∈ f, app_elim_lemma 6 3.
fn_on_app_elim. ⊢ fn_on f A → x ∈ A → y = app f x →
(x, y) ∈ f, subj_intro_iii 7.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.