Theorem neq0f

Description: A class is not empty if and only if it has at least one element. Proposition 5.17(1) of TakeutiZaring p. 20. This version of neq0 requires only that x not be free in, rather than not occur in, A . (Contributed by BJ, 15-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2	1	eq0f	$$⊢A=\varnothing \leftrightarrow \forall x\neg x\in A$$
3	2	notbii	$$⊢\neg A=\varnothing \leftrightarrow \neg \forall x\neg x\in A$$
4		df-ex	$$⊢\exists xx\in A\leftrightarrow \neg \forall x\neg x\in A$$
5	3 4	bitr4i	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$