ind1

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

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

Step	Hyp	Ref	Expression
1		simp2	$⊢ (O \in V \land A \subseteq O \land X \in A) \to A \subseteq O$
2		simp3	$⊢ (O \in V \land A \subseteq O \land X \in A) \to X \in A$
3	1 2	sseldd	$⊢ (O \in V \land A \subseteq O \land X \in A) \to X \in O$
4		indfval	$⊢ (O \in V \land A \subseteq O \land X \in O) \to 𝟙_{O} (A) (X) = if (X \in A, 1, 0)$
5	3 4	syld3an3	$⊢ (O \in V \land A \subseteq O \land X \in A) \to 𝟙_{O} (A) (X) = if (X \in A, 1, 0)$
6		iftrue	$⊢ X \in A \to if (X \in A, 1, 0) = 1$
7	6	3ad2ant3	$⊢ (O \in V \land A \subseteq O \land X \in A) \to if (X \in A, 1, 0) = 1$
8	5 7	eqtrd	$⊢ (O \in V \land A \subseteq O \land X \in A) \to 𝟙_{O} (A) (X) = 1$

Metamath Proof Explorer