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\in A\to \left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
2		undifr	$$⊢\left\{B\right\}\subseteq A\leftrightarrow \left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=A$$
3	1 2	sylib	$$⊢B\in A\to \left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=A$$