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		uncom	$$⊢\left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=\left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)$$
2		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
3		undif	$$⊢\left\{B\right\}\subseteq A\leftrightarrow \left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)=A$$
4	2 3	sylib	$$⊢B\in A\to \left\{B\right\}\cup \left(A\setminus \left\{B\right\}\right)=A$$
5	1 4	eqtrid	$$⊢B\in A\to \left(A\setminus \left\{B\right\}\right)\cup \left\{B\right\}=A$$