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	$$⊢\neg x\in A$$
Assertion	nel0	$$⊢A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nel0.1	$$⊢\neg x\in A$$
2		eq0	$$⊢A=\varnothing \leftrightarrow \forall x\neg x\in A$$
3	2 1	mpgbir	$$⊢A=\varnothing$$