This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psseq12i

Description: An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004)

	Ref	Expression
Hypotheses	psseq1i.1	$⊢ A = B$
	psseq12i.2	$⊢ C = D$
Assertion	psseq12i	$⊢ A \subset C \leftrightarrow B \subset D$

Step	Hyp	Ref	Expression
1		psseq1i.1	$⊢ A = B$
2		psseq12i.2	$⊢ C = D$
3	1	psseq1i	$⊢ A \subset C \leftrightarrow B \subset C$
4	2	psseq2i	$⊢ B \subset C \leftrightarrow B \subset D$
5	3 4	bitri	$⊢ A \subset C \leftrightarrow B \subset D$