Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | limeq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordeq | |
|
2 | neeq1 | |
|
3 | id | |
|
4 | unieq | |
|
5 | 3 4 | eqeq12d | |
6 | 1 2 5 | 3anbi123d | |
7 | df-lim | |
|
8 | df-lim | |
|
9 | 6 7 8 | 3bitr4g | |