Theorem psseq2

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

	Ref	Expression
Assertion	psseq2	|- ( A = B -> ( C C. A <-> C C. B ) )

Proof

Step	Hyp	Ref	Expression
1		sseq2	|- ( A = B -> ( C C_ A <-> C C_ B ) )
2		neeq2	|- ( A = B -> ( C =/= A <-> C =/= B ) )
3	1 2	anbi12d	|- ( A = B -> ( ( C C_ A /\ C =/= A ) <-> ( C C_ B /\ C =/= B ) ) )
4		df-pss	|- ( C C. A <-> ( C C_ A /\ C =/= A ) )
5		df-pss	|- ( C C. B <-> ( C C_ B /\ C =/= B ) )
6	3 4 5	3bitr4g	|- ( A = B -> ( C C. A <-> C C. B ) )