![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limeq | Structured version Visualization version Unicode version |
Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
limeq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordeq 5430 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | neeq1 2686 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | id 22 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | unieq 4206 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqeq12d 2466 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | 3anbi123d 1339 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | df-lim 5428 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | df-lim 5428 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 6, 7, 8 | 3bitr4g 292 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-in 3411 df-ss 3418 df-uni 4199 df-tr 4498 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-ord 5426 df-lim 5428 |
This theorem is referenced by: limuni2 5484 0ellim 5485 limuni3 6679 tfinds2 6690 dfom2 6694 limomss 6697 nnlim 6705 limom 6707 ssnlim 6710 onfununi 7060 tfr1a 7112 tz7.44lem1 7123 tz7.44-2 7125 tz7.44-3 7126 oeeulem 7302 limensuc 7749 elom3 8153 r1funlim 8237 rankxplim2 8351 rankxplim3 8352 rankxpsuc 8353 infxpenlem 8444 alephislim 8514 cflim2 8693 winalim 9120 rankcf 9202 gruina 9243 rdgprc0 30440 dfrdg2 30442 dfrdg4 30718 limsucncmpi 31105 limsucncmp 31106 |
Copyright terms: Public domain | W3C validator |