Proof
01. 1 ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)}, hypo.
02. 2 ⊢ a ∈ dom f, hypo.
03. 2 ⊢ ∃b. (a, b) ∈ f, dom_elim 2.
04. 4 ⊢ (a, b) ∈ f, hypo.
05. 1, 4 ⊢ (a, b) ∈ {t | ∃x. x ∈ X ∧ t = (x, y x)},
eq_subst 1 4, P u ↔ (a, b) ∈ u.
06. 1, 4 ⊢ ∃x. x ∈ X ∧ (a, b) = (x, y x), comp_elim 5.
07. 7 ⊢ x ∈ X ∧ (a, b) = (x, y x), hypo.
08. 7 ⊢ x ∈ X, conj_eliml 7.
09. 7 ⊢ (a, b) = (x, y x), conj_elimr 7.
10. 4 ⊢ set (a, b), set_intro 4.
11. 4 ⊢ set a, setl_from_pair 10.
12. 4 ⊢ set b, setr_from_pair 10.
13. 4, 7 ⊢ a = x ∧ b = y x, pair_property 11 12 9.
14. 4, 7 ⊢ a = x, conj_eliml 13.
15. 4, 7 ⊢ a ∈ X, eq_subst_rev 14 8, P u ↔ u ∈ X.
16. 1, 4 ⊢ a ∈ X, ex_elim 6 15.
17. 1, 2 ⊢ a ∈ X, ex_elim 3 16.
18. 1 ⊢ a ∈ dom f → a ∈ X, subj_intro 17.
19. 19 ⊢ a ∈ X, hypo.
20. ⊢ (a, y a) = (a, y a), eq_refl.
21. 19 ⊢ a ∈ X ∧ (a, y a) = (a, y a), conj_intro 19 20.
22. 19 ⊢ ∃x. x ∈ X ∧ (a, y a) = (x, y x), ex_intro 21.
23. 19 ⊢ set a, set_intro 19.
24. 24 ⊢ ∀x. x ∈ X → set (y x), hypo.
25. 24, 19 ⊢ set (y a), uq_bounded_elim 24 19.
26. 24, 19 ⊢ set (a, y a), set_pair 23 25.
27. 24, 19 ⊢ (a, y a) ∈ {t | ∃x. x ∈ X ∧ t = (x, y x)},
comp_intro 26 22, P u ↔ (∃x. x ∈ X ∧ u = (x, y x)).
28. 1, 24, 19 ⊢ (a, y a) ∈ f, eq_subst_rev 1 27, P u ↔ (a, y a) ∈ u.
29. 1, 24, 19 ⊢ a ∈ dom f, dom_intro 28.
30. 1, 24 ⊢ a ∈ X → a ∈ dom f, subj_intro 29.
31. 1, 24 ⊢ a ∈ dom f ↔ a ∈ X, bij_intro 18 30.
32. 1, 24 ⊢ ∀x. x ∈ dom f ↔ x ∈ X, uq_intro 31.
33. 1, 24 ⊢ dom f = X, ext 32.
dom_from_term. ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)} →
(∀x. x ∈ X → set (y x)) → dom f = X, subj_intro_ii 33.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.