MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limeq Unicode version

Theorem limeq 4404
Description: Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
limeq  |-  ( A  =  B  ->  ( Lim  A  <->  Lim  B ) )

Proof of Theorem limeq
StepHypRef Expression
1 ordeq 4399 . . 3  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
2 neeq1 2454 . . 3  |-  ( A  =  B  ->  ( A  =/=  (/)  <->  B  =/=  (/) ) )
3 id 19 . . . 4  |-  ( A  =  B  ->  A  =  B )
4 unieq 3836 . . . 4  |-  ( A  =  B  ->  U. A  =  U. B )
53, 4eqeq12d 2297 . . 3  |-  ( A  =  B  ->  ( A  =  U. A  <->  B  =  U. B ) )
61, 2, 53anbi123d 1252 . 2  |-  ( A  =  B  ->  (
( Ord  A  /\  A  =/=  (/)  /\  A  = 
U. A )  <->  ( Ord  B  /\  B  =/=  (/)  /\  B  =  U. B ) ) )
7 df-lim 4397 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
8 df-lim 4397 . 2  |-  ( Lim 
B  <->  ( Ord  B  /\  B  =/=  (/)  /\  B  =  U. B ) )
96, 7, 83bitr4g 279 1  |-  ( A  =  B  ->  ( Lim  A  <->  Lim  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934    = wceq 1623    =/= wne 2446   (/)c0 3455   U.cuni 3827   Ord word 4391   Lim wlim 4393
This theorem is referenced by:  limuni2  4453  0ellim  4454  limuni3  4643  tfinds2  4654  dfom2  4658  limomss  4661  nnlim  4669  limom  4671  ssnlim  4674  onfununi  6358  tfr1a  6410  tz7.44lem1  6418  tz7.44-2  6420  tz7.44-3  6421  oeeulem  6599  limensuc  7038  elom3  7349  r1funlim  7438  rankxplim2  7550  rankxplim3  7551  rankxpsuc  7552  infxpenlem  7641  alephislim  7710  cflim2  7889  winalim  8317  rankcf  8399  gruina  8440  rdgprc0  24150  dfrdg2  24152  dfrdg4  24488  limsucncmpi  24884  limsucncmp  24885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-lim 4397
  Copyright terms: Public domain W3C validator