Metamath Proof Explorer

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 e. B
Assertion ne0ii 
|- B =/= (/)

Proof

Step Hyp Ref Expression
1 n0ii.1 
 |-  A e. B
2 ne0i 
 |-  ( A e. B -> B =/= (/) )
3 1 2 ax-mp 
 |-  B =/= (/)