Metamath Proof Explorer
Description: If a class has elements, then it is not empty. Inference associated
with n0i . (Contributed by BJ, 15Jul2021)


Ref 
Expression 

Hypothesis 
n0ii.1 
$${\u22a2}{A}\in {B}$$ 

Assertion 
n0ii 
$${\u22a2}\neg {B}=\varnothing $$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

n0ii.1 
$${\u22a2}{A}\in {B}$$ 
2 

n0i 
$${\u22a2}{A}\in {B}\to \neg {B}=\varnothing $$ 
3 
1 2

axmp 
$${\u22a2}\neg {B}=\varnothing $$ 