Theorem snnzb

Description: A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018)

	Ref	Expression
Assertion	snnzb	$$⊢A\in \mathrm{V}\leftrightarrow \left\{A\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
2		df-ne	$$⊢\left\{A\right\}\ne \varnothing \leftrightarrow \neg \left\{A\right\}=\varnothing$$
3	2	con2bii	$$⊢\left\{A\right\}=\varnothing \leftrightarrow \neg \left\{A\right\}\ne \varnothing$$
4	1 3	bitri	$$⊢\neg A\in \mathrm{V}\leftrightarrow \neg \left\{A\right\}\ne \varnothing$$
5	4	con4bii	$$⊢A\in \mathrm{V}\leftrightarrow \left\{A\right\}\ne \varnothing$$