Theorem indicator_app_is_zero

Proof
01. 1 ⊢ A ⊆ X, hypo.
02. 2 ⊢ x ∈ X \ A, hypo.
03. ⊢ (x, ∅) = (x, ∅), eq_refl.
04. 2 ⊢ x ∈ X \ A ∧ (x, ∅) = (x, ∅), conj_intro 2 3.
05. 2 ⊢ ∃u. u ∈ X \ A ∧ (x, ∅) = (u, ∅), ex_intro 4.
06. 2 ⊢ set x, set_intro 2.
07. ⊢ set ∅, empty_set_is_set.
08. 2 ⊢ set (x, ∅), set_pair 6 7.
09. 2 ⊢ (x, ∅) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)},
  comp_intro 8 5, P t ↔ (∃x. x ∈ X \ A ∧ t = (x, ∅)).
10. 2 ⊢ (x, ∅) ∈ {t | ∃x. x ∈ X \ A ∧ t = (x, ∅)} ∪
  {t | ∃x. x ∈ A ∧ t = (x, {∅})}, union_introl 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_zero. ⊢ A ⊆ X → 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.