Theorem empty_map

Proof
01. ⊢ ∅ ⊆ Y, empty_set_is_least.
02. ⊢ rng ∅ ⊆ Y, eq_subst_rev rng_empty_set 1.
empty_map. ⊢ map ∅ ∅ Y, map_intro empty_function dom_empty_set 2.

Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.