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 uncom 
 |-  ( ( A \ { B } ) u. { B } ) = ( { B } u. ( A \ { B } ) )
2 snssi 
 |-  ( B e. A -> { B } C_ A )
3 undif 
 |-  ( { B } C_ A <-> ( { B } u. ( A \ { B } ) ) = A )
4 2 3 sylib 
 |-  ( B e. A -> ( { B } u. ( A \ { B } ) ) = A )
5 1 4 syl5eq 
 |-  ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )