Theorem difsn

Description: An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	difsn	$$⊢\neg A\in B\to B\setminus \left\{A\right\}=B$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢x\in \left(B\setminus \left\{A\right\}\right)\leftrightarrow \left(x\in B\wedge x\ne A\right)$$
2		simpl	$$⊢\left(x\in B\wedge x\ne A\right)\to x\in B$$
3		nelelne	$$⊢\neg A\in B\to \left(x\in B\to x\ne A\right)$$
4	3	ancld	$$⊢\neg A\in B\to \left(x\in B\to \left(x\in B\wedge x\ne A\right)\right)$$
5	2 4	impbid2	$$⊢\neg A\in B\to \left(\left(x\in B\wedge x\ne A\right)\leftrightarrow x\in B\right)$$
6	1 5	bitrid	$$⊢\neg A\in B\to \left(x\in \left(B\setminus \left\{A\right\}\right)\leftrightarrow x\in B\right)$$
7	6	eqrdv	$$⊢\neg A\in B\to B\setminus \left\{A\right\}=B$$