Proof 01. 1 ⊢ x ∈ X, hypo. 02. ⊢ x ∈ X → x ∈ X, subj_intro 1. 03. ⊢ ∀x. x ∈ X → x ∈ X, uq_intro 2. 04. 1 ⊢ app (id X) x = x, map_from_term_app id_eq 3 1. id_app. ⊢ x ∈ X → app (id X) x = x, subj_intro 4.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.