Metamath Proof Explorer


Theorem limeq

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 A=BLimALimB

Proof

Step Hyp Ref Expression
1 ordeq A=BOrdAOrdB
2 neeq1 A=BAB
3 id A=BA=B
4 unieq A=BA=B
5 3 4 eqeq12d A=BA=AB=B
6 1 2 5 3anbi123d A=BOrdAAA=AOrdBBB=B
7 df-lim LimAOrdAAA=A
8 df-lim LimBOrdBBB=B
9 6 7 8 3bitr4g A=BLimALimB