Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | sspred | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 | |
|
2 | df-pred | |
|
3 | 2 | sseq1i | |
4 | df-ss | |
|
5 | in32 | |
|
6 | 5 | eqeq1i | |
7 | 3 4 6 | 3bitri | |
8 | ineq1 | |
|
9 | 8 | eqeq1d | |
10 | 9 | biimpa | |
11 | df-pred | |
|
12 | 10 11 2 | 3eqtr4g | |
13 | 12 | eqcomd | |
14 | 1 7 13 | syl2anb | |