Theorem ex_uniq_from_fn_on

Theorem. ex_uniq_from_fn_on
fn_on f A → ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f
Proof
01. 1 ⊢ fn_on f A, hypo.
02. 1 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f,
  lsubj_conj_elimr fn_on_equi 1.
ex_uniq_from_fn_on. ⊢ fn_on f A → ∀x. x ∈ A →
  ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, subj_intro 2.