Theorem sseq1

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 21-Jun-2011)

	Ref	Expression
Assertion	sseq1	$$⊢A=B\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
2		sstr2	$$⊢B\subseteq A\to \left(A\subseteq C\to B\subseteq C\right)$$
3		sstr2	$$⊢A\subseteq B\to \left(B\subseteq C\to A\subseteq C\right)$$
4	2 3	anbiim	$$⊢\left(B\subseteq A\wedge A\subseteq B\right)\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$
5	4	ancoms	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$
6	1 5	sylbi	$$⊢A=B\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$