Theorem indicator_app_is_one

Proof
01. 1 ⊢ A ⊆ X, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. ⊢ (x, {∅}) = (x, {∅}), eq_refl.
04. 2 ⊢ x ∈ A ∧ (x, {∅}) = (x, {∅}), conj_intro 2 3.
05. 2 ⊢ ∃u. u ∈ A ∧ (x, {∅}) = (u, {∅}), ex_intro 4.
06. 2 ⊢ set x, set_intro 2.
07. ⊢ set {∅}, set_sg empty_set_is_set.
08. 2 ⊢ set (x, {∅}), set_pair 6 7.
09. 2 ⊢ (x, {∅}) ∈ {t | ∃x. x ∈ A ∧ t = (x, {∅})},
  comp_intro 8 5, P t ↔ (∃x. x ∈ A ∧ t = (x, {∅})).
10. 2 ⊢ (x, {∅}) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∪
  {t | ∃x. x ∈ A ∧ t = (x, {∅})}, union_intror 9.
11. 2 ⊢ (x, {∅}) ∈ χ A X, eq_subst_rev indicator_eq 10,
  P u ↔ (x, {∅}) ∈ u.
12. 1 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 1.
13. 1, 2 ⊢ {∅} = app (χ A X) x, map_app_intro 12 11.
14. 1, 2 ⊢ app (χ A X) x = {∅}, eq_symm 13.
indicator_app_is_one. ⊢ A ⊆ X → x ∈ A → app (χ A X) x = {∅},
  subj_intro_ii 14.

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