Theorem sseq2i

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

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

Proof

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