Proof 01. 1 ⊢ map f X Y, hypo. 02. 2 ⊢ set X, hypo. 03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1. 04. 1 ⊢ function f, conj_elimll 3. 05. 1 ⊢ dom f = X, conj_elimlr 3. 06. 1, 2 ⊢ set (dom f), eq_subst_rev 5 2. 07. 1, 2 ⊢ set f, function_is_set 4 6. map_is_set. ⊢ map f X Y → set X → set f, subj_intro_ii 7.
Dependencies
The given proof depends on 11 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, power, subset, substitution, union.