Theorem fn_on_intro_cod

Proof
01. 1 ⊢ relation f, hypo.
02. 2 ⊢ ∀x. x ∈ A → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f, hypo.
03. 3 ⊢ x ∈ A, hypo.
04. 2, 3 ⊢ ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_bounded_elim 2 3.
05. ⊢ z ∈ Y → set z, set_intro.
06. ⊢ ∀z. z ∈ Y → set z, uq_intro 5.
07. 2, 3 ⊢ ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, ex_weaken_conj 6 4.
08. 2 ⊢ x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, subj_intro 7.
09. 2 ⊢ ∀x. x ∈ A → ∃z. set z ∧ ∀y. z = y ↔ (x, y) ∈ f, uq_intro 8.
10. 1, 2 ⊢ fn_on f A, fn_on_intro 1 9.
fn_on_intro_cod. ⊢ relation f →
  (∀x. x ∈ A → ∃z. z ∈ Y ∧ ∀y. z = y ↔ (x, y) ∈ f) →
  fn_on f A, subj_intro_ii 10.