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

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	|- F/_ x A
2		df-ne	|- ( A =/= (/) <-> -. A = (/) )
3	1	neq0f	|- ( -. A = (/) <-> E. x x e. A )
4	2 3	bitri	|- ( A =/= (/) <-> E. x x e. A )