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

Metamath Proof Explorer

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 )