Theorem ne0ii

Description: If a class has elements, then it is nonempty. Inference associated with ne0i . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	n0ii.1	$$⊢A\in B$$
Assertion	ne0ii	$$⊢B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0ii.1	$$⊢A\in B$$
2		ne0i	$$⊢A\in B\to B\ne \varnothing$$
3	1 2	ax-mp	$$⊢B\ne \varnothing$$