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 = B -> ( Lim A <-> Lim B ) )

Proof

Step Hyp Ref Expression
1 ordeq 
 |-  ( A = B -> ( Ord A <-> Ord B ) )
2 neeq1 
 |-  ( A = B -> ( A =/= (/) <-> B =/= (/) ) )
3 id 
 |-  ( A = B -> A = B )
4 unieq 
 |-  ( A = B -> U. A = U. B )
5 3 4 eqeq12d 
 |-  ( A = B -> ( A = U. A <-> B = U. B ) )
6 1 2 5 3anbi123d 
 |-  ( A = B -> ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord B /\ B =/= (/) /\ B = U. B ) ) )
7 df-lim 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
8 df-lim 
 |-  ( Lim B <-> ( Ord B /\ B =/= (/) /\ B = U. B ) )
9 6 7 8 3bitr4g 
 |-  ( A = B -> ( Lim A <-> Lim B ) )