Metamath Proof Explorer


Theorem n0ii

Description: If a class has elements, then it is not empty. Inference associated with n0i . (Contributed by BJ, 15-Jul-2021)

Ref Expression
Hypothesis n0ii.1
|- A e. B
Assertion n0ii
|- -. B = (/)

Proof

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