Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | sspss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfpss2 | |
|
2 | 1 | simplbi2 | |
3 | 2 | con1d | |
4 | 3 | orrd | |
5 | pssss | |
|
6 | eqimss | |
|
7 | 5 6 | jaoi | |
8 | 4 7 | impbii | |