Theorem dfss4

Description: Subclass defined in terms of class difference. See comments under dfun2 . (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	dfss4	$$⊢A\subseteq B\leftrightarrow B\setminus \left(B\setminus A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		sseqin2	$$⊢A\subseteq B\leftrightarrow B\cap A=A$$
2		eldif	$$⊢x\in \left(B\setminus A\right)\leftrightarrow \left(x\in B\wedge \neg x\in A\right)$$
3	2	notbii	$$⊢\neg x\in \left(B\setminus A\right)\leftrightarrow \neg \left(x\in B\wedge \neg x\in A\right)$$
4	3	anbi2i	$$⊢\left(x\in B\wedge \neg x\in \left(B\setminus A\right)\right)\leftrightarrow \left(x\in B\wedge \neg \left(x\in B\wedge \neg x\in A\right)\right)$$
5		elin	$$⊢x\in \left(B\cap A\right)\leftrightarrow \left(x\in B\wedge x\in A\right)$$
6		abai	$$⊢\left(x\in B\wedge x\in A\right)\leftrightarrow \left(x\in B\wedge \left(x\in B\to x\in A\right)\right)$$
7		iman	$$⊢\left(x\in B\to x\in A\right)\leftrightarrow \neg \left(x\in B\wedge \neg x\in A\right)$$
8	7	anbi2i	$$⊢\left(x\in B\wedge \left(x\in B\to x\in A\right)\right)\leftrightarrow \left(x\in B\wedge \neg \left(x\in B\wedge \neg x\in A\right)\right)$$
9	5 6 8	3bitri	$$⊢x\in \left(B\cap A\right)\leftrightarrow \left(x\in B\wedge \neg \left(x\in B\wedge \neg x\in A\right)\right)$$
10	4 9	bitr4i	$$⊢\left(x\in B\wedge \neg x\in \left(B\setminus A\right)\right)\leftrightarrow x\in \left(B\cap A\right)$$
11	10	difeqri	$$⊢B\setminus \left(B\setminus A\right)=B\cap A$$
12	11	eqeq1i	$$⊢B\setminus \left(B\setminus A\right)=A\leftrightarrow B\cap A=A$$
13	1 12	bitr4i	$$⊢A\subseteq B\leftrightarrow B\setminus \left(B\setminus A\right)=A$$