Metamath Proof Explorer


Theorem ssdifsym

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

Ref Expression
Assertion ssdifsym ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐵 = ( 𝑉𝐴 ) ↔ 𝐴 = ( 𝑉𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ssdifim ( ( 𝐴𝑉𝐵 = ( 𝑉𝐴 ) ) → 𝐴 = ( 𝑉𝐵 ) )
2 1 ex ( 𝐴𝑉 → ( 𝐵 = ( 𝑉𝐴 ) → 𝐴 = ( 𝑉𝐵 ) ) )
3 2 adantr ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐵 = ( 𝑉𝐴 ) → 𝐴 = ( 𝑉𝐵 ) ) )
4 ssdifim ( ( 𝐵𝑉𝐴 = ( 𝑉𝐵 ) ) → 𝐵 = ( 𝑉𝐴 ) )
5 4 ex ( 𝐵𝑉 → ( 𝐴 = ( 𝑉𝐵 ) → 𝐵 = ( 𝑉𝐴 ) ) )
6 5 adantl ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐴 = ( 𝑉𝐵 ) → 𝐵 = ( 𝑉𝐴 ) ) )
7 3 6 impbid ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐵 = ( 𝑉𝐴 ) ↔ 𝐴 = ( 𝑉𝐵 ) ) )