rng_elim

Theorem rng_elim

Theorem. rng_elim
y ∈ rng R → ∃x. (x, y) ∈ R

Proof
01. 1 ⊢ y ∈ rng R, hypo.
02. 1 ⊢ y ∈ {y | ∃x. (x, y) ∈ R}, eq_subst rng_eq 1, P u ↔ y ∈ u.
03. 1 ⊢ ∃x. (x, y) ∈ R, comp_elim 2.
rng_elim. ⊢ y ∈ rng R → ∃x. (x, y) ∈ R, subj_intro 3.

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