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 e. C -> ( A e. _V <-> ( A \ B ) e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		difexg	|- ( A e. _V -> ( A \ B ) e. _V )
2		ssun2	|- A C_ ( B u. A )
3		uncom	|- ( ( A \ B ) u. B ) = ( B u. ( A \ B ) )
4		undif2	|- ( B u. ( A \ B ) ) = ( B u. A )
5	3 4	eqtr2i	|- ( B u. A ) = ( ( A \ B ) u. B )
6	2 5	sseqtri	|- A C_ ( ( A \ B ) u. B )
7		unexg	|- ( ( ( A \ B ) e. _V /\ B e. C ) -> ( ( A \ B ) u. B ) e. _V )
8		ssexg	|- ( ( A C_ ( ( A \ B ) u. B ) /\ ( ( A \ B ) u. B ) e. _V ) -> A e. _V )
9	6 7 8	sylancr	|- ( ( ( A \ B ) e. _V /\ B e. C ) -> A e. _V )
10	9	expcom	|- ( B e. C -> ( ( A \ B ) e. _V -> A e. _V ) )
11	1 10	impbid2	|- ( B e. C -> ( A e. _V <-> ( A \ B ) e. _V ) )