Theorem img_intro

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ (x, y) ∈ R, hypo.
03. 2 ⊢ set (x, y), set_intro 2.
04. 2 ⊢ set y, setr_from_pair 3.
05. 1, 2 ⊢ x ∈ A ∧ (x, y) ∈ R, conj_intro 1 2.
06. 1, 2 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ R, ex_intro 5.
07. 1, 2 ⊢ y ∈ {y | ∃x. x ∈ A ∧ (x, y) ∈ R}, comp_intro 4 6.
08. 1, 2 ⊢ y ∈ img R A, eq_subst_rev img_eq 7, P u ↔ y ∈ u.
img_intro. ⊢ x ∈ A → (x, y) ∈ R → y ∈ img R A, subj_intro_ii 8.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.