Theorem dfpss3

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	dfpss3	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfpss2	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
2		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
3	2	baib	$$⊢A\subseteq B\to \left(A=B\leftrightarrow B\subseteq A\right)$$
4	3	notbid	$$⊢A\subseteq B\to \left(\neg A=B\leftrightarrow \neg B\subseteq A\right)$$
5	4	pm5.32i	$$⊢\left(A\subseteq B\wedge \neg A=B\right)\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$
6	1 5	bitri	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$