Proof 01. 1 ⊢ y ∈ img f A, hypo. 02. 1 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ f, img_elim 1. 03. 3 ⊢ x ∈ A ∧ (x, y) ∈ f, hypo. 04. 3 ⊢ x ∈ A, conj_eliml 3. 05. 3 ⊢ (x, y) ∈ f, conj_elimr 3. 06. 3 ⊢ (x, y) ∈ restr f A, restr_intro 5 4. 07. 3 ⊢ y ∈ img (restr f A) A, img_intro 4 6. 08. 1 ⊢ y ∈ img (restr f A) A, ex_elim 2 7. 09. ⊢ y ∈ img f A → y ∈ img (restr f A) A, subj_intro 8. 10. ⊢ ∀y. y ∈ img f A → y ∈ img (restr f A) A, uq_intro 9. restr_img_self. ⊢ img f A ⊆ img (restr f A) A, incl_intro 10.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.