Proof 01. 1 ⊢ map f X Y, hypo. 02. 2 ⊢ (x, y) ∈ f, hypo. 03. 1 ⊢ function f, map_is_function 1. 04. 1, 2 ⊢ y = app f x, app_intro 3 2. map_app_intro. ⊢ map f X Y → (x, y) ∈ f → y = app f x, subj_intro_ii 4.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.