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 ABVBVA

Proof

Step Hyp Ref Expression
1 sscon ABVBVA
2 sscon VBVAVVAVVB
3 ddif VVA=A
4 ddif VVB=B
5 2 3 4 3sstr3g VBVAAB
6 1 5 impbii ABVBVA