This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )