Theorem from_indicator_app_is_one

Proof
01. 1 ⊢ A ⊆ X, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 3 ⊢ app (χ A X) x = {∅}, hypo.
04. 3 ⊢ {∅} = app (χ A X) x, eq_symm 3.
05. 1 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 1.
06. 1, 2, 3 ⊢ (x, {∅}) ∈ χ A X, map_app_elim 5 2 4.
07. 1, 2, 3 ⊢ (x, {∅}) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∪
  {t | ∃x. x ∈ A ∧ t = (x, {∅})},
  eq_subst indicator_eq 6, P u ↔ (x, {∅}) ∈ u.
08. 1, 2, 3 ⊢
  (x, {∅}) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∨
  (x, {∅}) ∈ {t | ∃x. x ∈ A ∧ t = (x, {∅})}, union_elim 7.
09. 9 ⊢ (x, {∅}) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)}, hypo.
10. 9 ⊢ ∃u. u ∈ X \ A ∧ (x, {∅}) = (u, ∅), comp_elim 9.
11. 11 ⊢ u ∈ X \ A ∧ (x, {∅}) = (u, ∅), hypo.
12. 11 ⊢ (x, {∅}) = (u, ∅), conj_elimr 11.
13. 2 ⊢ set x, set_intro 2.
14. ⊢ set {∅}, set_sg empty_set_is_set.
15. 2, 11 ⊢ x = u ∧ {∅} = ∅, pair_property 13 14 12.
16. 2, 11 ⊢ {∅} = ∅, conj_elimr 15.
17. 2, 11 ⊢ ∅ = {∅}, eq_symm 16.
18. 2, 11 ⊢ ⊥, neg_elim zero_neq_one 17.
19. 2, 11 ⊢ x ∈ A, efq 18.
20. 2, 9 ⊢ x ∈ A, ex_elim 10 19.
21. 21 ⊢ (x, {∅}) ∈ {t | ∃x. x ∈ A ∧ t = (x, {∅})}, hypo.
22. 21 ⊢ ∃u. u ∈ A ∧ (x, {∅}) = (u, {∅}), comp_elim 21.
23. 23 ⊢ u ∈ A ∧ (x, {∅}) = (u, {∅}), hypo.
24. 23 ⊢ u ∈ A, conj_eliml 23.
25. 23 ⊢ (x, {∅}) = (u, {∅}), conj_elimr 23.
26. 2, 23 ⊢ x = u ∧ {∅} = {∅}, pair_property 13 14 25.
27. 2, 23 ⊢ x = u, conj_eliml 26.
28. 2, 23 ⊢ x ∈ A, eq_subst_rev 27 24.
29. 2, 21 ⊢ x ∈ A, ex_elim 22 28.
30. 1, 2, 3 ⊢ x ∈ A, disj_elim 8 20 29.
from_indicator_app_is_one. ⊢ A ⊆ X → x ∈ X →
  app (χ A X) x = {∅} → x ∈ A, subj_intro_iii 30.

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