Theorem sseq12d

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999)

	Ref	Expression
Hypotheses	sseq1d.1	$$⊢\phi \to A=B$$
	sseq12d.2	$$⊢\phi \to C=D$$
Assertion	sseq12d	$$⊢\phi \to \left(A\subseteq C\leftrightarrow B\subseteq D\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq1d.1	$$⊢\phi \to A=B$$
2		sseq12d.2	$$⊢\phi \to C=D$$
3	1	sseq1d	$$⊢\phi \to \left(A\subseteq C\leftrightarrow B\subseteq C\right)$$
4	2	sseq2d	$$⊢\phi \to \left(B\subseteq C\leftrightarrow B\subseteq D\right)$$
5	3 4	bitrd	$$⊢\phi \to \left(A\subseteq C\leftrightarrow B\subseteq D\right)$$