Theorem psseq2

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996)

	Ref	Expression
Assertion	psseq2	$$⊢A=B\to \left(C\subset A\leftrightarrow C\subset B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢A=B\to \left(C\subseteq A\leftrightarrow C\subseteq B\right)$$
2		neeq2	$$⊢A=B\to \left(C\ne A\leftrightarrow C\ne B\right)$$
3	1 2	anbi12d	$$⊢A=B\to \left(\left(C\subseteq A\wedge C\ne A\right)\leftrightarrow \left(C\subseteq B\wedge C\ne B\right)\right)$$
4		df-pss	$$⊢C\subset A\leftrightarrow \left(C\subseteq A\wedge C\ne A\right)$$
5		df-pss	$$⊢C\subset B\leftrightarrow \left(C\subseteq B\wedge C\ne B\right)$$
6	3 4 5	3bitr4g	$$⊢A=B\to \left(C\subset A\leftrightarrow C\subset B\right)$$