Theorem snnzb

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

	Ref	Expression
Assertion	snnzb	⊢ ( 𝐴 ∈ V ↔ { 𝐴 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
2		df-ne	⊢ ( { 𝐴 } ≠ ∅ ↔ ¬ { 𝐴 } = ∅ )
3	2	con2bii	⊢ ( { 𝐴 } = ∅ ↔ ¬ { 𝐴 } ≠ ∅ )
4	1 3	bitri	⊢ ( ¬ 𝐴 ∈ V ↔ ¬ { 𝐴 } ≠ ∅ )
5	4	con4bii	⊢ ( 𝐴 ∈ V ↔ { 𝐴 } ≠ ∅ )