Proof 01. 1 ⊢ relation f, hypo. 02. 2 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, hypo. 03. 1, 2 ⊢ relation f ∧ (∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f), conj_intro 1 2. 04. 1, 2 ⊢ fn_on f A, rsubj_elim fn_on_equi 3. fn_on_intro. ⊢ relation f → (∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f) → fn_on f A, subj_intro_ii 4.