Proof
01. 1 ⊢ (x, y) ∈ R, hypo.
02. 1 ⊢ set (x, y), set_intro 1.
03. 1 ⊢ set y, setr_from_pair 2.
04. 1 ⊢ ∃x. (x, y) ∈ R, ex_intro 1.
05. 1 ⊢ y ∈ {y | ∃x. (x, y) ∈ R}, comp_intro 3 4.
06. 1 ⊢ y ∈ rng R, eq_subst_rev rng_eq 5, P u ↔ y ∈ u.
rng_intro. ⊢ (x, y) ∈ R → y ∈ rng R, subj_intro 6.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.