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