fn_app_exists

Theorem fn_app_exists

Theorem. fn_app_exists
function f → x ∈ dom f → ∃y. y ∈ rng f ∧ y = app f x

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ x ∈ dom f, hypo.
03. 2 ⊢ ∃y. (x, y) ∈ f, dom_elim 2.
04. 4 ⊢ (x, y) ∈ f, hypo.
05. 4 ⊢ y ∈ rng f, rng_intro 4.
06. 1, 4 ⊢ y = app f x, app_intro 1 4.
07. 1, 4 ⊢ y ∈ rng f ∧ y = app f x, conj_intro 5 6.
08. 1, 4 ⊢ ∃y. y ∈ rng f ∧ y = app f x, ex_intro 7.
09. 1, 2 ⊢ ∃y. y ∈ rng f ∧ y = app f x, ex_elim 3 8.
fn_app_exists. ⊢ function f → x ∈ dom f → ∃y. y ∈ rng f ∧ y = app f x,
  subj_intro_ii 9.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.