Theorem npss

Description: A class is not a proper subclass of another iff it satisfies a one-directional form of eqss . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	npss	$$⊢\neg A\subset B\leftrightarrow \left(A\subseteq B\to A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm4.61	$$⊢\neg \left(A\subseteq B\to A=B\right)\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
2		dfpss2	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
3	1 2	bitr4i	$$⊢\neg \left(A\subseteq B\to A=B\right)\leftrightarrow A\subset B$$
4	3	con1bii	$$⊢\neg A\subset B\leftrightarrow \left(A\subseteq B\to A=B\right)$$