map_dom

Theorem map_dom

Theorem. map_dom
map f X Y → dom f = X

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
03. 1 ⊢ dom f = X, conj_elimlr 2.
map_dom. ⊢ map f X Y → dom f = X, subj_intro 3.