Metamath Proof Explorer

Theorem ssdifsym

Description: Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022)

Ref Expression
Assertion ssdifsym 
|- ( ( A C_ V /\ B C_ V ) -> ( B = ( V \ A ) <-> A = ( V \ B ) ) )

Proof

Step Hyp Ref Expression
1 ssdifim 
 |-  ( ( A C_ V /\ B = ( V \ A ) ) -> A = ( V \ B ) )
2 1 ex 
 |-  ( A C_ V -> ( B = ( V \ A ) -> A = ( V \ B ) ) )
3 2 adantr 
 |-  ( ( A C_ V /\ B C_ V ) -> ( B = ( V \ A ) -> A = ( V \ B ) ) )
4 ssdifim 
 |-  ( ( B C_ V /\ A = ( V \ B ) ) -> B = ( V \ A ) )
5 4 ex 
 |-  ( B C_ V -> ( A = ( V \ B ) -> B = ( V \ A ) ) )
6 5 adantl 
 |-  ( ( A C_ V /\ B C_ V ) -> ( A = ( V \ B ) -> B = ( V \ A ) ) )
7 3 6 impbid 
 |-  ( ( A C_ V /\ B C_ V ) -> ( B = ( V \ A ) <-> A = ( V \ B ) ) )