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	2	adantl	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\to \left(A\subseteq C\to B\subseteq C\right)$$
4		sstr2	$$⊢A\subseteq B\to \left(B\subseteq C\to A\subseteq C\right)$$
5	4	adantr	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\to \left(B\subseteq C\to A\subseteq C\right)$$
6	3 5	impbid	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$
7	1 6	sylbi	$$⊢A=B\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$