Theorem map_extensionality_lemma

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
03. 1 ⊢ function f ∧ dom f = X, conj_eliml 2.
04. 1 ⊢ function f, conj_eliml 3.
05. 1 ⊢ dom f = X, conj_elimr 3.
06. 1 ⊢ dom f ⊆ X, incl_from_eq 5.
07. 1 ⊢ rng f ⊆ Y, conj_elimr 2.
08. 1 ⊢ relation f, fn_is_rel 4.
09. 1 ⊢ f ⊆ X × Y, relation_incl_prod 8 6 7.
10. 10 ⊢ t ∈ f, hypo.
11. 1, 10 ⊢ t ∈ X × Y, incl_elim 9 10.
12. 1, 10 ⊢ ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), prod_elim 11.
13. 13 ⊢ ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
14. 14 ⊢ x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
15. 14 ⊢ x ∈ X ∧ y ∈ Y, conj_eliml 14.
16. 14 ⊢ x ∈ X, conj_eliml 15.
17. 14 ⊢ y ∈ Y, conj_elimr 15.
18. 14 ⊢ t = (x, y), conj_elimr 14.
19. 10, 14 ⊢ (x, y) ∈ f, eq_subst 18 10, P u ↔ u ∈ f.
20. 1, 10, 14 ⊢ y = app f x, app_intro 4 19.
21. 21 ⊢ map g X Y, hypo.
22. 21 ⊢ function g ∧ dom g = X ∧ rng g ⊆ Y, map_unfold 21.
23. 21 ⊢ function g ∧ dom g = X, conj_eliml 22.
24. 21 ⊢ function g, conj_eliml 23.
25. 21 ⊢ dom g = X, conj_elimr 23.
26. 21 ⊢ rng g ⊆ Y, conj_elimr 22.
27. 27 ⊢ ∀x. x ∈ X → app f x = app g x, hypo.
28. 27 ⊢ x ∈ X → app f x = app g x, uq_elim 27.
29. 27, 14 ⊢ app f x = app g x, subj_elim 28 16.
30. 1, 27, 10, 14 ⊢ y = app g x, eq_trans 20 29.
31. 21, 14 ⊢ x ∈ dom g, eq_subst_rev 25 16, P u ↔ x ∈ u.
32. 1, 21, 27, 10, 14 ⊢ (x, y) ∈ g, app_elim 24 31 30.
33. 1, 21, 27, 10, 14 ⊢ t ∈ g, eq_subst_rev 18 32, P u ↔ u ∈ g.
34. 1, 21, 27, 10, 13 ⊢ t ∈ g, ex_elim 13 33.
35. 1, 21, 27, 10 ⊢ t ∈ g, ex_elim 12 34.
36. 1, 21, 27 ⊢ t ∈ f → t ∈ g, subj_intro 35.
37. 1, 21, 27 ⊢ ∀t. t ∈ f → t ∈ g, uq_intro 36.
38. 1, 21, 27 ⊢ f ⊆ g, incl_intro 37.
map_extensionality_lemma. ⊢ map f X Y → map g X Y →
  (∀x. x ∈ X → app f x = app g x) → f ⊆ g, subj_intro_iii 38.

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