Theorem nel0

Description: From the general negation of membership in A , infer that A is the empty set. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Hypothesis	nel0.1	|- -. x e. A
Assertion	nel0	|- A = (/)

Proof

Step	Hyp	Ref	Expression
1		nel0.1	|- -. x e. A
2		eq0	|- ( A = (/) <-> A. x -. x e. A )
3	2 1	mpgbir	|- A = (/)