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

Metamath Proof Explorer

Theorem snnzg

Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008)

		Ref	Expression
	Assertion	snnzg	$⊢ A \in V \to \{A\} \neq \emptyset$

Step	Hyp	Ref	Expression
1		snidg	$⊢ A \in V \to A \in \{A\}$
2	1	ne0d	$⊢ A \in V \to \{A\} \neq \emptyset$