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 )