Metamath Proof Explorer


Theorem difsnid

Description: If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006)

Ref Expression
Assertion difsnid B A A B B = A

Proof

Step Hyp Ref Expression
1 snssi B A B A
2 undifr B A A B B = A
3 1 2 sylib B A A B B = A