Theorem eldif

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994)

	Ref	Expression
Assertion	eldif	$$⊢A\in \left(B\setminus C\right)\leftrightarrow \left(A\in B\wedge \neg A\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \left(B\setminus C\right)\to A\in \mathrm{V}$$
2		elex	$$⊢A\in B\to A\in \mathrm{V}$$
3	2	adantr	$$⊢\left(A\in B\wedge \neg A\in C\right)\to A\in \mathrm{V}$$
4		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
5		eleq1	$$⊢x=A\to \left(x\in C\leftrightarrow A\in C\right)$$
6	5	notbid	$$⊢x=A\to \left(\neg x\in C\leftrightarrow \neg A\in C\right)$$
7	4 6	anbi12d	$$⊢x=A\to \left(\left(x\in B\wedge \neg x\in C\right)\leftrightarrow \left(A\in B\wedge \neg A\in C\right)\right)$$
8		df-dif	$$⊢B\setminus C=\left\{x|\left(x\in B\wedge \neg x\in C\right)\right\}$$
9	7 8	elab2g	$$⊢A\in \mathrm{V}\to \left(A\in \left(B\setminus C\right)\leftrightarrow \left(A\in B\wedge \neg A\in C\right)\right)$$
10	1 3 9	pm5.21nii	$$⊢A\in \left(B\setminus C\right)\leftrightarrow \left(A\in B\wedge \neg A\in C\right)$$