Metamath Proof Explorer

Theorem complss

Description: Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by BJ, 19-Mar-2021)

Ref Expression
Assertion complss 
|- ( A C_ B <-> ( _V \ B ) C_ ( _V \ A ) )

Proof

Step Hyp Ref Expression
1 sscon 
 |-  ( A C_ B -> ( _V \ B ) C_ ( _V \ A ) )
2 sscon 
 |-  ( ( _V \ B ) C_ ( _V \ A ) -> ( _V \ ( _V \ A ) ) C_ ( _V \ ( _V \ B ) ) )
3 ddif 
 |-  ( _V \ ( _V \ A ) ) = A
4 ddif 
 |-  ( _V \ ( _V \ B ) ) = B
5 2 3 4 3sstr3g 
 |-  ( ( _V \ B ) C_ ( _V \ A ) -> A C_ B )
6 1 5 impbii 
 |-  ( A C_ B <-> ( _V \ B ) C_ ( _V \ A ) )