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\subseteq B\leftrightarrow \mathrm{V}\setminus B\subseteq \mathrm{V}\setminus A$$

Proof

Step	Hyp	Ref	Expression
1		sscon	$$⊢A\subseteq B\to \mathrm{V}\setminus B\subseteq \mathrm{V}\setminus A$$
2		sscon	$$⊢\mathrm{V}\setminus B\subseteq \mathrm{V}\setminus A\to \mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)\subseteq \mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)$$
3		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)=A$$
4		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)=B$$
5	2 3 4	3sstr3g	$$⊢\mathrm{V}\setminus B\subseteq \mathrm{V}\setminus A\to A\subseteq B$$
6	1 5	impbii	$$⊢A\subseteq B\leftrightarrow \mathrm{V}\setminus B\subseteq \mathrm{V}\setminus A$$