Theorem eq0ALT

Description: Alternate proof of eq0 . Shorter, but requiring df-clel , ax-8 . (Contributed by NM, 29-Aug-1993) Avoid ax-11 , ax-12 . (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	eq0ALT	|- ( A = (/) <-> A. x -. x e. A )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( A = (/) <-> A. x ( x e. A <-> x e. (/) ) )
2		noel	|- -. x e. (/)
3	2	nbn	|- ( -. x e. A <-> ( x e. A <-> x e. (/) ) )
4	3	albii	|- ( A. x -. x e. A <-> A. x ( x e. A <-> x e. (/) ) )
5	1 4	bitr4i	|- ( A = (/) <-> A. x -. x e. A )