Theorem indsn

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

	Ref	Expression
Assertion	indsn	|- ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( O e. V /\ X e. O ) -> X e. O )
2	1	snssd	|- ( ( O e. V /\ X e. O ) -> { X } C_ O )
3		indval	|- ( ( O e. V /\ { X } C_ O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) )
4	2 3	syldan	|- ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) )
5		velsn	|- ( x e. { X } <-> x = X )
6	5	a1i	|- ( ( O e. V /\ X e. O ) -> ( x e. { X } <-> x = X ) )
7	6	ifbid	|- ( ( O e. V /\ X e. O ) -> if ( x e. { X } , 1 , 0 ) = if ( x = X , 1 , 0 ) )
8	7	mpteq2dv	|- ( ( O e. V /\ X e. O ) -> ( x e. O |-> if ( x e. { X } , 1 , 0 ) ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )
9	4 8	eqtrd	|- ( ( O e. V /\ X e. O ) -> ( ( _Ind ` O ) ` { X } ) = ( x e. O |-> if ( x = X , 1 , 0 ) ) )