Metamath Proof Explorer

Theorem elndif

Description: A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994)

Ref Expression
Assertion elndif 
|- ( A e. B -> -. A e. ( C \ B ) )

Proof

Step Hyp Ref Expression
1 eldifn 
 |-  ( A e. ( C \ B ) -> -. A e. B )
2 1 con2i 
 |-  ( A e. B -> -. A e. ( C \ B ) )