Theorem sspss

Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996)

	Ref	Expression
Assertion	sspss	$$⊢A\subseteq B\leftrightarrow \left(A\subset B\vee A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfpss2	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg A=B\right)$$
2	1	simplbi2	$$⊢A\subseteq B\to \left(\neg A=B\to A\subset B\right)$$
3	2	con1d	$$⊢A\subseteq B\to \left(\neg A\subset B\to A=B\right)$$
4	3	orrd	$$⊢A\subseteq B\to \left(A\subset B\vee A=B\right)$$
5		pssss	$$⊢A\subset B\to A\subseteq B$$
6		eqimss	$$⊢A=B\to A\subseteq B$$
7	5 6	jaoi	$$⊢\left(A\subset B\vee A=B\right)\to A\subseteq B$$
8	4 7	impbii	$$⊢A\subseteq B\leftrightarrow \left(A\subset B\vee A=B\right)$$