Proof
01. 1 ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)}, hypo.
02. 2 ⊢ ∀x. x ∈ X → y x ∈ Y, hypo.
03. 3 ⊢ b ∈ rng f, hypo.
04. 3 ⊢ ∃a. (a, b) ∈ f, rng_elim 3.
05. 5 ⊢ (a, b) ∈ f, hypo.
06. 1, 5 ⊢ (a, b) ∈ {t | ∃x. x ∈ X ∧ t = (x, y x)},
eq_subst 1 5, P u ↔ (a, b) ∈ u.
07. 1, 5 ⊢ ∃x. x ∈ X ∧ (a, b) = (x, y x), comp_elim 6.
08. 8 ⊢ x ∈ X ∧ (a, b) = (x, y x), hypo.
09. 8 ⊢ x ∈ X, conj_eliml 8.
10. 8 ⊢ (a, b) = (x, y x), conj_elimr 8.
11. 5 ⊢ set (a, b), set_intro 5.
12. 5 ⊢ set a, setl_from_pair 11.
13. 5 ⊢ set b, setr_from_pair 11.
14. 5, 8 ⊢ a = x ∧ b = y x, pair_property 12 13 10.
15. 5, 8 ⊢ b = y x, conj_elimr 14.
16. 2, 8 ⊢ y x ∈ Y, uq_bounded_elim 2 9.
17. 2, 5, 8 ⊢ b ∈ Y, eq_subst_rev 15 16, P u ↔ u ∈ Y.
18. 1, 2, 5 ⊢ b ∈ Y, ex_elim 7 17.
19. 1, 2, 3 ⊢ b ∈ Y, ex_elim 4 18.
20. 1, 2 ⊢ b ∈ rng f → b ∈ Y, subj_intro 19.
21. 1, 2 ⊢ ∀y. y ∈ rng f → y ∈ Y, uq_intro 20.
22. 1, 2 ⊢ rng f ⊆ Y, incl_intro 21.
rng_from_term. ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)} →
(∀x. x ∈ X → y x ∈ Y) → rng f ⊆ Y, subj_intro_ii 22.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.