Metamath Proof Explorer

Theorem compleq

Description: Two classes are equal if and only if their complements are equal. (Contributed by BJ, 19-Mar-2021)

Ref Expression
Assertion compleq 
|- ( A = B <-> ( _V \ A ) = ( _V \ B ) )

Proof

Step Hyp Ref Expression
1 complss 
 |-  ( A C_ B <-> ( _V \ B ) C_ ( _V \ A ) )
2 complss 
 |-  ( B C_ A <-> ( _V \ A ) C_ ( _V \ B ) )
3 1 2 anbi12ci 
 |-  ( ( A C_ B /\ B C_ A ) <-> ( ( _V \ A ) C_ ( _V \ B ) /\ ( _V \ B ) C_ ( _V \ A ) ) )
4 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
5 eqss 
 |-  ( ( _V \ A ) = ( _V \ B ) <-> ( ( _V \ A ) C_ ( _V \ B ) /\ ( _V \ B ) C_ ( _V \ A ) ) )
6 3 4 5 3bitr4i 
 |-  ( A = B <-> ( _V \ A ) = ( _V \ B ) )