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	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) )
2		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
3		undif	⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
4	2 3	sylib	⊢ ( 𝐵 ∈ 𝐴 → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
5	1 4	eqtrid	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )