Metamath Proof Explorer
Description: A set does not belong to a class excluding it. (Contributed by NM, 27Jun1994)


Ref 
Expression 

Assertion 
elndif 
$${\u22a2}{A}\in {B}\to \neg {A}\in \left({C}\setminus {B}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eldifn 
$${\u22a2}{A}\in \left({C}\setminus {B}\right)\to \neg {A}\in {B}$$ 
2 
1

con2i 
$${\u22a2}{A}\in {B}\to \neg {A}\in \left({C}\setminus {B}\right)$$ 