Theorem eq0f

Description: A class is equal to the empty set if and only if it has no elements. Theorem 2 of Suppes p. 22. (Contributed by BJ, 15-Jul-2021)

	Ref	Expression
Hypothesis	eq0f.1	|- F/_ x A
Assertion	eq0f	|- ( A = (/) <-> A. x -. x e. A )

Proof

Step	Hyp	Ref	Expression
1		eq0f.1	|- F/_ x A
2		nfcv	|- F/_ x (/)
3	1 2	cleqf	|- ( A = (/) <-> A. x ( x e. A <-> x e. (/) ) )
4		noel	|- -. x e. (/)
5	4	nbn	|- ( -. x e. A <-> ( x e. A <-> x e. (/) ) )
6	5	albii	|- ( A. x -. x e. A <-> A. x ( x e. A <-> x e. (/) ) )
7	3 6	bitr4i	|- ( A = (/) <-> A. x -. x e. A )