Metamath Proof Explorer

Theorem ind0

Description: Value of the indicator function where it is 0 . (Contributed by Thierry Arnoux, 14-Aug-2017)

Ref Expression
Assertion ind0 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∖ A → 𝟙 O ⁡ A ⁡ X = 0

Proof

Step Hyp Ref Expression
1 eldifi ⊢ X ∈ O ∖ A → X ∈ O
2 indfval ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0
3 1 2 syl3an3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∖ A → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0
4 eldifn ⊢ X ∈ O ∖ A → ¬ X ∈ A
5 4 3ad2ant3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∖ A → ¬ X ∈ A
6 5 iffalsed ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∖ A → if X ∈ A 1 0 = 0
7 3 6 eqtrd ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O ∖ A → 𝟙 O ⁡ A ⁡ X = 0