Theorem eldifsn

Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007)

	Ref	Expression
Assertion	eldifsn	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\leftrightarrow \left(A\in B\wedge A\ne C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldif	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\leftrightarrow \left(A\in B\wedge \neg A\in \left\{C\right\}\right)$$
2		elsng	$$⊢A\in B\to \left(A\in \left\{C\right\}\leftrightarrow A=C\right)$$
3	2	necon3bbid	$$⊢A\in B\to \left(\neg A\in \left\{C\right\}\leftrightarrow A\ne C\right)$$
4	3	pm5.32i	$$⊢\left(A\in B\wedge \neg A\in \left\{C\right\}\right)\leftrightarrow \left(A\in B\wedge A\ne C\right)$$
5	1 4	bitri	$$⊢A\in \left(B\setminus \left\{C\right\}\right)\leftrightarrow \left(A\in B\wedge A\ne C\right)$$