Description: Alternate version of bj-rest10 . (Contributed by BJ, 27-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-rest10b |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif | ||
2 | 0ex | ||
3 | 2 | elsn2 | |
4 | neqne | ||
5 | 3 4 | sylnbi | |
6 | 5 | anim2i | |
7 | 1 6 | sylbi | |
8 | bj-rest10 | ||
9 | 8 | imp | |
10 | 7 9 | syl |