map_app_elim

Theorem map_app_elim

Theorem. map_app_elim
map f X Y → x ∈ X → y = app f x → (x, y) ∈ f

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 3 ⊢ y = app f x, hypo.
04. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
05. 1 ⊢ function f ∧ dom f = X, conj_eliml 4.
06. 1 ⊢ function f, conj_eliml 5.
07. 1 ⊢ dom f = X, conj_elimr 5.
08. 1, 2 ⊢ x ∈ dom f, eq_subst_rev 7 2, P u ↔ x ∈ u.
09. 1, 2, 3 ⊢ (x, y) ∈ f, app_elim 6 8 3.
map_app_elim. ⊢ map f X Y → x ∈ X → y = app f x → (x, y) ∈ f,
  subj_intro_iii 9.

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