Theorem snnzg

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

	Ref	Expression
Assertion	snnzg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
2	1	ne0d	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )