Theorem eqsn

Description: Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007) (Proof shortened by JJ, 23-Jul-2021)

	Ref	Expression
Assertion	eqsn	$$⊢A\ne \varnothing \to \left(A=\left\{B\right\}\leftrightarrow \forall x\in Ax=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
2		biorf	$$⊢\neg A=\varnothing \to \left(A=\left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)\right)$$
3	1 2	sylbi	$$⊢A\ne \varnothing \to \left(A=\left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)\right)$$
4		dfss3	$$⊢A\subseteq \left\{B\right\}\leftrightarrow \forall x\in Ax\in \left\{B\right\}$$
5		sssn	$$⊢A\subseteq \left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)$$
6		velsn	$$⊢x\in \left\{B\right\}\leftrightarrow x=B$$
7	6	ralbii	$$⊢\forall x\in Ax\in \left\{B\right\}\leftrightarrow \forall x\in Ax=B$$
8	4 5 7	3bitr3i	$$⊢\left(A=\varnothing \vee A=\left\{B\right\}\right)\leftrightarrow \forall x\in Ax=B$$
9	3 8	bitrdi	$$⊢A\ne \varnothing \to \left(A=\left\{B\right\}\leftrightarrow \forall x\in Ax=B\right)$$