This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )