Theorem sseq1i

Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993)

	Ref	Expression
Hypothesis	sseq1i.1	$$⊢A=B$$
Assertion	sseq1i	$$⊢A\subseteq C\leftrightarrow B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		sseq1i.1	$$⊢A=B$$
2		sseq1	$$⊢A=B\to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$
3	1 2	ax-mp	$$⊢A\subseteq C\leftrightarrow B\subseteq C$$