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 ∈ C → A ∈ V ↔ A ∖ B ∈ V

Proof

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