Metamath Proof Explorer


Theorem psseq1

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

Ref Expression
Assertion psseq1 A=BACBC

Proof

Step Hyp Ref Expression
1 sseq1 A=BACBC
2 neeq1 A=BACBC
3 1 2 anbi12d A=BACACBCBC
4 df-pss ACACAC
5 df-pss BCBCBC
6 3 4 5 3bitr4g A=BACBC