Theorem elsni

Description: There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994)

	Ref	Expression
Assertion	elsni	$$⊢A\in \left\{B\right\}\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		elsng	$$⊢A\in \left\{B\right\}\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
2	1	ibi	$$⊢A\in \left\{B\right\}\to A=B$$