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 e. V -> { A } =/= (/) )

Proof

Step Hyp Ref Expression
1 snidg 
 |-  ( A e. V -> A e. { A } )
2 1 ne0d 
 |-  ( A e. V -> { A } =/= (/) )