Metamath Proof Explorer

Theorem indsn

Description: The indicator function of a singleton. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Assertion indsn ⊢ O ∈ V ∧ X ∈ O → 𝟙 O ⁡ X = x ∈ O ⟼ if x = X 1 0

Proof

Step Hyp Ref Expression
1 simpr ⊢ O ∈ V ∧ X ∈ O → X ∈ O
2 1 snssd ⊢ O ∈ V ∧ X ∈ O → X ⊆ O
3 indval ⊢ O ∈ V ∧ X ⊆ O → 𝟙 O ⁡ X = x ∈ O ⟼ if x ∈ X 1 0
4 2 3 syldan ⊢ O ∈ V ∧ X ∈ O → 𝟙 O ⁡ X = x ∈ O ⟼ if x ∈ X 1 0
5 velsn ⊢ x ∈ X ↔ x = X
6 5 a1i ⊢ O ∈ V ∧ X ∈ O → x ∈ X ↔ x = X
7 6 ifbid ⊢ O ∈ V ∧ X ∈ O → if x ∈ X 1 0 = if x = X 1 0
8 7 mpteq2dv ⊢ O ∈ V ∧ X ∈ O → x ∈ O ⟼ if x ∈ X 1 0 = x ∈ O ⟼ if x = X 1 0
9 4 8 eqtrd ⊢ O ∈ V ∧ X ∈ O → 𝟙 O ⁡ X = x ∈ O ⟼ if x = X 1 0