Proof 01. 1 ⊢ function f, hypo. 02. 2 ⊢ x ∈ dom f, hypo. 03. 1, 2 ⊢ ∃y. y ∈ rng f ∧ y = app f x, fn_app_exists 1 2. 04. 4 ⊢ y ∈ rng f ∧ y = app f x, hypo. 05. 4 ⊢ y ∈ rng f, conj_eliml 4. 06. 4 ⊢ y = app f x, conj_elimr 4. 07. 4 ⊢ set y, set_intro 5. 08. 4 ⊢ set (app f x), eq_subst 6 7, P u ↔ set u. 09. 1, 2 ⊢ set (app f x), ex_elim 3 8. app_is_set. ⊢ function f → x ∈ dom f → set (app f x), subj_intro_ii 9.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.