A stronger form of the replacement axiom.
Proof sketch
Consider the restriction f|A, which has
domain dom(f|A) = (dom f) ∩ A.
Because A is a set, this intersection must be a set as
well, since it is a subset of A, which brings the subset axiom
into play. Thus, according to the substitution axiom,
the range rng(f|A) must be a set. But then,
according to the subset axiom again, the image f[A]
must be a set as well, since f[A] ⊆ rng(f|A). q.e.d.
Proof 01. 1 ⊢ function f, hypo. 02. 2 ⊢ set A, hypo. 03. 1 ⊢ function (restr f A), restr_is_function 1. 04. ⊢ dom (restr f A) = dom f ∩ A, dom_restr. 05. ⊢ dom f ∩ A ⊆ A, intersection_incl_right. 06. 2 ⊢ set (dom f ∩ A), subset 5 2. 07. 2 ⊢ set (dom (restr f A)), eq_subst_rev 4 6, P t ↔ set t. 08. 1, 2 ⊢ set (rng (restr f A)), substitution 3 7. 09. ⊢ img (restr f A) A ⊆ rng (restr f A), img_incl_in_rng. 10. ⊢ img f A ⊆ img (restr f A) A, restr_img_self. 11. ⊢ img f A ⊆ rng (restr f A), incl_trans 10 9. 12. 1, 2 ⊢ set (img f A), subset 11 8. replacement_strong. ⊢ function f → set A → set (img f A), subj_intro_ii 12.
Dependencies
The given proof depends on 10 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, substitution, union.