ind0

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

		Ref	Expression
	Assertion	ind0	$⊢ (O \in V \land A \subseteq O \land X \in (O ∖ A)) \to 𝟙_{O} (A) (X) = 0$

Step	Hyp	Ref	Expression
1		eldifi	$⊢ X \in (O ∖ A) \to X \in O$
2		indfval	$⊢ (O \in V \land A \subseteq O \land X \in O) \to 𝟙_{O} (A) (X) = if (X \in A, 1, 0)$
3	1 2	syl3an3	$⊢ (O \in V \land A \subseteq O \land X \in (O ∖ A)) \to 𝟙_{O} (A) (X) = if (X \in A, 1, 0)$
4		eldifn	$⊢ X \in (O ∖ A) \to \neg X \in A$
5	4	3ad2ant3	$⊢ (O \in V \land A \subseteq O \land X \in (O ∖ A)) \to \neg X \in A$
6	5	iffalsed	$⊢ (O \in V \land A \subseteq O \land X \in (O ∖ A)) \to if (X \in A, 1, 0) = 0$
7	3 6	eqtrd	$⊢ (O \in V \land A \subseteq O \land X \in (O ∖ A)) \to 𝟙_{O} (A) (X) = 0$

Metamath Proof Explorer