Map_elim

Theorem Map_elim

Theorem. Map_elim
f ∈ Map X Y → map f X Y

Proof
01. 1 ⊢ f ∈ Map X Y, hypo.
02. 1 ⊢ f ∈ {f | map f X Y}, eq_subst Map_eq 1, P t ↔ f ∈ t.
03. 1 ⊢ map f X Y, comp_elim 2.
Map_elim. ⊢ f ∈ Map X Y → map f X Y, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.