Metamath Proof Explorer

Theorem eldifi

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

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

Proof

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