Metamath Proof Explorer


Theorem difsn

Description: An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion difsn ¬ABBA=B

Proof

Step Hyp Ref Expression
1 eldifsn xBAxBxA
2 simpl xBxAxB
3 nelelne ¬ABxBxA
4 3 ancld ¬ABxBxBxA
5 2 4 impbid2 ¬ABxBxAxB
6 1 5 bitrid ¬ABxBAxB
7 6 eqrdv ¬ABBA=B