sspss

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

		Ref	Expression
	Assertion	sspss	$⊢ A \subseteq B \leftrightarrow (A \subset B \lor A = B)$

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

Metamath Proof Explorer