Metamath Proof Explorer


Theorem sspss

Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996)

Ref Expression
Assertion sspss ABABA=B

Proof

Step Hyp Ref Expression
1 dfpss2 ABAB¬A=B
2 1 simplbi2 AB¬A=BAB
3 2 con1d AB¬ABA=B
4 3 orrd ABABA=B
5 pssss ABAB
6 eqimss A=BAB
7 5 6 jaoi ABA=BAB
8 4 7 impbii ABABA=B