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

Metamath Proof Explorer

Theorem ssdifim

Description: Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022)

Ref Expression
Assertion ssdifim ⊢ A ⊆ V ∧ B = V ∖ A → A = V ∖ B

Proof

Step Hyp Ref Expression
1 dfss4 ⊢ A ⊆ V ↔ V ∖ V ∖ A = A
2 eqcom ⊢ V ∖ V ∖ A = A ↔ A = V ∖ V ∖ A
3 1 2 sylbb ⊢ A ⊆ V → A = V ∖ V ∖ A
4 difeq2 ⊢ B = V ∖ A → V ∖ B = V ∖ V ∖ A
5 4 eqcomd ⊢ B = V ∖ A → V ∖ V ∖ A = V ∖ B
6 3 5 sylan9eq ⊢ A ⊆ V ∧ B = V ∖ A → A = V ∖ B