Theorem inv_img_intro

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

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