Theorem fn_from_term

Proof
01. 1 ⊢ f = {t | ∃x. P x ∧ t = (x, y x)}, hypo.
02. 2 ⊢ t ∈ f, hypo.
03. 1, 2 ⊢ t ∈ {t | ∃x. P x ∧ t = (x, y x)},
  eq_subst 1 2, P u ↔ t ∈ u.
04. 1, 2 ⊢ ∃x. P x ∧ t = (x, y x), comp_elim 3.
05. 5 ⊢ P x ∧ t = (x, y x), hypo.
06. 5 ⊢ t = (x, y x), conj_elimr 5.
07. 5 ⊢ ∃x. t = (x, y x), ex_intro 6.
08. 1, 2 ⊢ ∃x. t = (x, y x), ex_elim 4 7.
09. 1, 2 ⊢ t ∈ {t | ∃x. t = (x, y x)}, comp_intro_from 2 8.
10. 1 ⊢ t ∈ f → t ∈ {t | ∃x. t = (x, y x)}, subj_intro 9.
11. 1 ⊢ ∀t. t ∈ f → t ∈ {t | ∃x. t = (x, y x)}, uq_intro 10.
12. 1 ⊢ f ⊆ {t | ∃x. t = (x, y x)}, incl_intro 11.
13. ⊢ {t | ∃x. t = (x, y x)} = {t | ∃x. t = (x, y x)}, eq_refl.
14. ⊢ function {t | ∃x. t = (x, y x)}, fn_from_term_plain 13.
15. 1 ⊢ function f, function_subclass 12 14.
fn_from_term. ⊢ f = {t | ∃x. P x ∧ t = (x, y x)} → function f,
  subj_intro 15.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.