Theorem difex2

Description: If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (Contributed by NM, 12-Nov-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	difex2	$$⊢B\in C\to \left(A\in \mathrm{V}\leftrightarrow A\setminus B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		difexg	$$⊢A\in \mathrm{V}\to A\setminus B\in \mathrm{V}$$
2		ssun2	$$⊢A\subseteq B\cup A$$
3		uncom	$$⊢\left(A\setminus B\right)\cup B=B\cup \left(A\setminus B\right)$$
4		undif2	$$⊢B\cup \left(A\setminus B\right)=B\cup A$$
5	3 4	eqtr2i	$$⊢B\cup A=\left(A\setminus B\right)\cup B$$
6	2 5	sseqtri	$$⊢A\subseteq \left(A\setminus B\right)\cup B$$
7		unexg	$$⊢\left(A\setminus B\in \mathrm{V}\wedge B\in C\right)\to \left(A\setminus B\right)\cup B\in \mathrm{V}$$
8		ssexg	$$⊢\left(A\subseteq \left(A\setminus B\right)\cup B\wedge \left(A\setminus B\right)\cup B\in \mathrm{V}\right)\to A\in \mathrm{V}$$
9	6 7 8	sylancr	$$⊢\left(A\setminus B\in \mathrm{V}\wedge B\in C\right)\to A\in \mathrm{V}$$
10	9	expcom	$$⊢B\in C\to \left(A\setminus B\in \mathrm{V}\to A\in \mathrm{V}\right)$$
11	1 10	impbid2	$$⊢B\in C\to \left(A\in \mathrm{V}\leftrightarrow A\setminus B\in \mathrm{V}\right)$$