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		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
2		undifr	⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
3	1 2	sylib	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )