img_elim

Theorem img_elim

Theorem. img_elim
y ∈ img R A → ∃x. x ∈ A ∧ (x, y) ∈ R

Proof
01. 1 ⊢ y ∈ img R A, hypo.
02. 1 ⊢ y ∈ {y | ∃x. x ∈ A ∧ (x, y) ∈ R},
  eq_subst img_eq 1, P u ↔ y ∈ u.
03. 1 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ R, comp_elim 2.
img_elim. ⊢ y ∈ img R A → ∃x. x ∈ A ∧ (x, y) ∈ R, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.