Metamath Proof Explorer

Theorem snn0d

Description: The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis snn0d.1 
|- ( ph -> A e. V )
Assertion snn0d 
|- ( ph -> { A } =/= (/) )

Proof

Step Hyp Ref Expression
1 snn0d.1 
 |-  ( ph -> A e. V )
2 snnzg 
 |-  ( A e. V -> { A } =/= (/) )
3 1 2 syl 
 |-  ( ph -> { A } =/= (/) )