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 ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )

Proof

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