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 B
Assertion n0ii ¬ B =

Proof

Step Hyp Ref Expression
1 n0ii.1 A B
2 n0i A B ¬ B =
3 1 2 ax-mp ¬ B =