Theorem indsn

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

	Ref	Expression
Assertion	indsn	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → 𝑋 ∈ 𝑂 )
2	1	snssd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → { 𝑋 } ⊆ 𝑂 )
3		indval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ { 𝑋 } ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) )
4	2 3	syldan	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) )
5		velsn	⊢ ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 )
6	5	a1i	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 ) )
7	6	ifbid	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) = if ( 𝑥 = 𝑋 , 1 , 0 ) )
8	7	mpteq2dv	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )
9	4 8	eqtrd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )