Metamath Proof Explorer

Theorem ind1

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

Ref Expression
Assertion ind1 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → 𝟙 O ⁡ A ⁡ X = 1

Proof

Step Hyp Ref Expression
1 simp2 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → A ⊆ O
2 simp3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → X ∈ A
3 1 2 sseldd ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → X ∈ O
4 indfval ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0
5 3 4 syld3an3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0
6 iftrue ⊢ X ∈ A → if X ∈ A 1 0 = 1
7 6 3ad2ant3 ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → if X ∈ A 1 0 = 1
8 5 7 eqtrd ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ A → 𝟙 O ⁡ A ⁡ X = 1