Metamath Proof Explorer

Theorem snnzb

Description: A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018)

Ref Expression
Assertion snnzb 
|- ( A e. _V <-> { A } =/= (/) )

Proof

Step Hyp Ref Expression
1 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
2 df-ne 
 |-  ( { A } =/= (/) <-> -. { A } = (/) )
3 2 con2bii 
 |-  ( { A } = (/) <-> -. { A } =/= (/) )
4 1 3 bitri 
 |-  ( -. A e. _V <-> -. { A } =/= (/) )
5 4 con4bii 
 |-  ( A e. _V <-> { A } =/= (/) )