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	⊢ ¬ 𝑥 ∈ 𝐴
Assertion	nel0	⊢ 𝐴 = ∅

Proof

Step	Hyp	Ref	Expression
1		nel0.1	⊢ ¬ 𝑥 ∈ 𝐴
2		eq0	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
3	2 1	mpgbir	⊢ 𝐴 = ∅