Theorem n0f

Description: A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of TakeutiZaring p. 20. This version of n0 requires only that x not be free in, rather than not occur in, A . (Contributed by NM, 17-Oct-2003)

	Ref	Expression
Hypothesis	eq0f.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	n0f	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
3	1	neq0f	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
4	2 3	bitri	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$