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 V A

Proof

Step Hyp Ref Expression
1 snprc ¬ A V A =
2 df-ne A ¬ A =
3 2 con2bii A = ¬ A
4 1 3 bitri ¬ A V ¬ A
5 4 con4bii A V A