Proof
01. 1 ⊢ f = {t | ∃x. t = (x, y x)}, hypo.
02. 2 ⊢ t ∈ f, hypo.
03. 1, 2 ⊢ t ∈ {t | ∃x. t = (x, y x)}, eq_subst 1 2.
04. 1, 2 ⊢ ∃x. t = (x, y x), comp_elim 3.
05. 5 ⊢ t = (x, y x), hypo.
06. 5 ⊢ ∃y. t = (x, y), ex_intro 5.
07. 5 ⊢ ∃x. ∃y. t = (x, y), ex_intro 6.
08. 1, 2 ⊢ ∃x. ∃y. t = (x, y), ex_elim 4 7.
09. 1 ⊢ t ∈ f → ∃x. ∃y. t = (x, y), subj_intro 8.
10. 1 ⊢ ∀t. t ∈ f → ∃x. ∃y. t = (x, y), uq_intro 9.
11. 1 ⊢ relation f, relation_fold 10.
12. 12 ⊢ (x, y1) ∈ f, hypo.
13. 13 ⊢ (x, y2) ∈ f, hypo.
14. 1, 12 ⊢ (x, y1) ∈ {t | ∃x. t = (x, y x)},
eq_subst 1 12, P u ↔ (x, y1) ∈ u.
15. 1, 13 ⊢ (x, y2) ∈ {t | ∃x. t = (x, y x)},
eq_subst 1 13, P u ↔ (x, y2) ∈ u.
16. 1, 12 ⊢ ∃x1. (x, y1) = (x1, y x1), comp_elim 14.
17. 1, 13 ⊢ ∃x2. (x, y2) = (x2, y x2), comp_elim 15.
18. 18 ⊢ (x, y1) = (x1, y x1), hypo.
19. 19 ⊢ (x, y2) = (x2, y x2), hypo.
20. 12 ⊢ set (x, y1), set_intro 12.
21. 13 ⊢ set (x, y2), set_intro 13.
22. 12 ⊢ set x, setl_from_pair 20.
23. 12 ⊢ set y1, setr_from_pair 20.
24. 13 ⊢ set x, setl_from_pair 21.
25. 13 ⊢ set y2, setr_from_pair 21.
26. 12, 18 ⊢ x = x1 ∧ y1 = y x1, pair_property 22 23 18.
27. 13, 19 ⊢ x = x2 ∧ y2 = y x2, pair_property 24 25 19.
28. 12, 18 ⊢ x = x1, conj_eliml 26.
29. 12, 18 ⊢ y1 = y x1, conj_elimr 26.
30. 13, 19 ⊢ x = x2, conj_eliml 27.
31. 13, 19 ⊢ y2 = y x2, conj_elimr 27.
32. 12, 18 ⊢ y1 = y x, eq_subst_rev 28 29.
33. 13, 19 ⊢ y2 = y x, eq_subst_rev 30 31.
34. 13, 19 ⊢ y x = y2, eq_symm 33.
35. 12, 13, 18, 19 ⊢ y1 = y2, eq_trans 32 34.
36. 1, 12, 13, 18 ⊢ y1 = y2, ex_elim 17 35.
37. 1, 12, 13 ⊢ y1 = y2, ex_elim 16 36.
38. 1, 12 ⊢ (x, y2) ∈ f → y1 = y2, subj_intro 37.
39. 1 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, subj_intro 38.
40. 1 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 39.
41. 1 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 40.
42. 1 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 41.
43. 1 ⊢ function f, function_intro 11 42.
fn_from_term_plain. ⊢ f = {t | ∃x. t = (x, y x)} → function f,
subj_intro 43.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.