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	|- F/_ x A
Assertion	neq0f	|- ( -. A = (/) <-> E. x x e. A )

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	|- F/_ x A
2	1	eq0f	|- ( A = (/) <-> A. x -. x e. A )
3	2	notbii	|- ( -. A = (/) <-> -. A. x -. x e. A )
4		df-ex	|- ( E. x x e. A <-> -. A. x -. x e. A )
5	3 4	bitr4i	|- ( -. A = (/) <-> E. x x e. A )