inv_img_elim

Theorem inv_img_elim

Theorem. inv_img_elim
x ∈ inv_img R B → ∃y. y ∈ B ∧ (x, y) ∈ R

Proof
01. 1 ⊢ x ∈ inv_img R B, hypo.
02. 1 ⊢ x ∈ {x | ∃y. y ∈ B ∧ (x, y) ∈ R},
  eq_subst inv_img_eq 1, P u ↔ x ∈ u.
03. 1 ⊢ ∃y. y ∈ B ∧ (x, y) ∈ R, comp_elim 2.
inv_img_elim. ⊢ x ∈ inv_img R B → ∃y. y ∈ B ∧ (x, y) ∈ R, subj_intro 3.

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