Theorem id_is_map

Proof
01. 1 ⊢ x ∈ X, hypo.
02. ⊢ x ∈ X → x ∈ X, subj_intro 1.
03. ⊢ ∀x. x ∈ X → x ∈ X, uq_intro 2.
id_is_map. ⊢ map (id X) X X, map_from_term id_eq 3.

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