Theorem nssinpss

Description: Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	nssinpss	$$⊢\neg A\subseteq B\leftrightarrow A\cap B\subset A$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap B\subseteq A$$
2	1	biantrur	$$⊢A\cap B\ne A\leftrightarrow \left(A\cap B\subseteq A\wedge A\cap B\ne A\right)$$
3		df-ss	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
4	3	necon3bbii	$$⊢\neg A\subseteq B\leftrightarrow A\cap B\ne A$$
5		df-pss	$$⊢A\cap B\subset A\leftrightarrow \left(A\cap B\subseteq A\wedge A\cap B\ne A\right)$$
6	2 4 5	3bitr4i	$$⊢\neg A\subseteq B\leftrightarrow A\cap B\subset A$$