Theorem dfpss2

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996)

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

Proof

Step	Hyp	Ref	Expression
1		df-pss	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)$$
2		df-ne	$$⊢A\ne B\leftrightarrow \neg A=B$$
3	2	anbi2i	$$⊢\left(A\subseteq B\wedge A\ne B\right)\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
4	1 3	bitri	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$