Theorem sseq12i

Description: An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999) (Proof shortened by Eric Schmidt, 26-Jan-2007)

	Ref	Expression
Hypotheses	sseq1i.1	$$⊢A=B$$
	sseq12i.2	$$⊢C=D$$
Assertion	sseq12i	$$⊢A\subseteq C\leftrightarrow B\subseteq D$$

Proof

Step	Hyp	Ref	Expression
1		sseq1i.1	$$⊢A=B$$
2		sseq12i.2	$$⊢C=D$$
3		sseq12	$$⊢\left(A=B\wedge C=D\right)\to \left(A\subseteq C\leftrightarrow B\subseteq D\right)$$
4	1 2 3	mp2an	$$⊢A\subseteq C\leftrightarrow B\subseteq D$$