Metamath Proof Explorer


Theorem eldifi

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

Ref Expression
Assertion eldifi A B C A B

Proof

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