Theorem ne0i

Description: If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993)

	Ref	Expression
Assertion	ne0i	⊢ ( 𝐵 ∈ 𝐴 → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅ )
2	1	neqned	⊢ ( 𝐵 ∈ 𝐴 → 𝐴 ≠ ∅ )