The axiom of replacement, derived as a theorem from its prototypical
form, the axiom of substitution. The premise
A ⊆ dom f is actually not needed, as shown in
replacement_strong.
Proof sketch
Consider the restriction f|A, which has
domain A because A ⊆ dom f. Thus, according to the
substitution axiom, its range
rng(f|A) must be a set. But then, according to the
subset axiom, 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 ⊢ A ⊆ dom f, hypo. 03. 3 ⊢ set A, hypo. 04. 1 ⊢ function (restr f A), restr_is_function 1. 05. ⊢ dom (restr f A) = dom f ∩ A, dom_restr. 06. 2 ⊢ A ∩ dom f = A, intersection_from_incl 2. 07. ⊢ dom f ∩ A = A ∩ dom f, intersection_comm. 08. 2 ⊢ dom f ∩ A = A, eq_trans 7 6. 09. 2 ⊢ dom (restr f A) = A, eq_trans 5 8. 10. 2, 3 ⊢ set (dom (restr f A)), eq_subst_rev 9 3, P t ↔ set t. 11. 1, 2, 3 ⊢ set (rng (restr f A)), substitution 4 10. 12. ⊢ img (restr f A) A ⊆ rng (restr f A), img_incl_in_rng. 13. ⊢ img f A ⊆ img (restr f A) A, restr_img_self. 14. ⊢ img f A ⊆ rng (restr f A), incl_trans 13 12. 15. 1, 2, 3 ⊢ set (img f A), subset 14 11. replacement. ⊢ function f → A ⊆ dom f → set A → set (img f A), subj_intro_iii 15.
Dependencies
The given proof depends on 10 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, substitution, union.