Metamath Proof Explorer


Theorem eldifn

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

Ref Expression
Assertion eldifn A B C ¬ A C

Proof

Step Hyp Ref Expression
1 eldif A B C A B ¬ A C
2 1 simprbi A B C ¬ A C