This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to A \in \{B\}$
	Assertion	elsnd	$⊢ φ \to A = B$

Step	Hyp	Ref	Expression
1		elsnd.1	$⊢ φ \to A \in \{B\}$
2		elsni	$⊢ A \in \{B\} \to A = B$
3	1 2	syl	$⊢ φ \to A = B$