Proof
01. 1 ⊢ fn_on f A, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 3 ⊢ (x, y) ∈ f, 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 ⊢ y = app f x, app_intro_lemma 6 3.
fn_on_app_intro. ⊢ fn_on f A → x ∈ A → (x, y) ∈ f →
y = app f x, subj_intro_iii 7.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.