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 e. A -> ( ( A \ { B } ) u. { B } ) = A )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( B e. A -> { B } C_ A )
2 undifr 
 |-  ( { B } C_ A <-> ( ( A \ { B } ) u. { B } ) = A )
3 1 2 sylib 
 |-  ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )