Map_intro

Theorem Map_intro

Theorem. Map_intro
map f X Y → set X → f ∈ Map X Y

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ set X, hypo.
03. 1, 2 ⊢ set f, map_is_set 1 2.
04. 1, 2 ⊢ f ∈ {f | map f X Y}, comp_intro 3 1.
05. 1, 2 ⊢ f ∈ Map X Y, eq_subst_rev Map_eq 4, P t ↔ f ∈ t.
Map_intro. ⊢ map f X Y → set X → f ∈ Map X Y, subj_intro_ii 5.

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