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 ( 𝐵 ∈ 𝐶 → ( 𝐴 ∈ V ↔ ( 𝐴 ∖ 𝐵 ) ∈ V ) )

Proof

Step Hyp Ref Expression
1 difexg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ 𝐵 ) ∈ V )
2 ssun2 ⊢ 𝐴 ⊆ ( 𝐵 ∪ 𝐴 )
3 uncom ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) )
4 undif2 ⊢ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐵 ∪ 𝐴 )
5 3 4 eqtr2i ⊢ ( 𝐵 ∪ 𝐴 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 )
6 2 5 sseqtri ⊢ 𝐴 ⊆ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 )
7 unexg ⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∈ V ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∈ V )
8 ssexg ⊢ ( ( 𝐴 ⊆ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∧ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
9 6 7 8 sylancr ⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∈ V ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ V )
10 9 expcom ⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝐴 ∖ 𝐵 ) ∈ V → 𝐴 ∈ V ) )
11 1 10 impbid2 ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ∈ V ↔ ( 𝐴 ∖ 𝐵 ) ∈ V ) )