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

Metamath Proof Explorer

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 V \leftrightarrow \{A\} \neq \emptyset$

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