Metamath Proof Explorer

Theorem eldifn

Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994)

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

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
2 1 simprbi 
 |-  ( A e. ( B \ C ) -> -. A e. C )