Metamath Proof Explorer

Theorem elsnd

Description: There is at most one element in a singleton. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypothesis elsnd.1 
|- ( ph -> A e. { B } )
Assertion elsnd 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 elsnd.1 
 |-  ( ph -> A e. { B } )
2 elsni 
 |-  ( A e. { B } -> A = B )
3 1 2 syl 
 |-  ( ph -> A = B )