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 C_ V /\ B = ( V \ A ) ) -> A = ( V \ B ) )

Proof

Step Hyp Ref Expression
1 dfss4 
 |-  ( A C_ V <-> ( V \ ( V \ A ) ) = A )
2 eqcom 
 |-  ( ( V \ ( V \ A ) ) = A <-> A = ( V \ ( V \ A ) ) )
3 1 2 sylbb 
 |-  ( A C_ 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 C_ V /\ B = ( V \ A ) ) -> A = ( V \ B ) )