Metamath Proof Explorer

Theorem ind1a

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

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

Proof

Step Hyp Ref Expression
1 indfval ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = if X ∈ A 1 0
2 1 eqeq1d ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = 1 ↔ if X ∈ A 1 0 = 1
3 eqid ⊢ 1 = 1
4 3 biantru ⊢ X ∈ A ↔ X ∈ A ∧ 1 = 1
5 ax-1ne0 ⊢ 1 ≠ 0
6 5 neii ⊢ ¬ 1 = 0
7 6 biorfri ⊢ X ∈ A ∧ 1 = 1 ↔ X ∈ A ∧ 1 = 1 ∨ 1 = 0
8 6 bianfi ⊢ 1 = 0 ↔ ¬ X ∈ A ∧ 1 = 0
9 8 orbi2i ⊢ X ∈ A ∧ 1 = 1 ∨ 1 = 0 ↔ X ∈ A ∧ 1 = 1 ∨ ¬ X ∈ A ∧ 1 = 0
10 4 7 9 3bitri ⊢ X ∈ A ↔ X ∈ A ∧ 1 = 1 ∨ ¬ X ∈ A ∧ 1 = 0
11 eqif ⊢ 1 = if X ∈ A 1 0 ↔ X ∈ A ∧ 1 = 1 ∨ ¬ X ∈ A ∧ 1 = 0
12 eqcom ⊢ 1 = if X ∈ A 1 0 ↔ if X ∈ A 1 0 = 1
13 10 11 12 3bitr2ri ⊢ if X ∈ A 1 0 = 1 ↔ X ∈ A
14 2 13 bitrdi ⊢ O ∈ V ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X = 1 ↔ X ∈ A