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

Theorem limeq 4536
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 4531 . . 3  |-  ( A  =  B  ->  ( Ord  A  <->  Ord  B ) )
2 neeq1 2560 . . 3  |-  ( A  =  B  ->  ( A  =/=  (/)  <->  B  =/=  (/) ) )
3 id 20 . . . 4  |-  ( A  =  B  ->  A  =  B )
4 unieq 3968 . . . 4  |-  ( A  =  B  ->  U. A  =  U. B )
53, 4eqeq12d 2403 . . 3  |-  ( A  =  B  ->  ( A  =  U. A  <->  B  =  U. B ) )
61, 2, 53anbi123d 1254 . 2  |-  ( A  =  B  ->  (
( Ord  A  /\  A  =/=  (/)  /\  A  = 
U. A )  <->  ( Ord  B  /\  B  =/=  (/)  /\  B  =  U. B ) ) )
7 df-lim 4529 . 2  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
8 df-lim 4529 . 2  |-  ( Lim 
B  <->  ( Ord  B  /\  B  =/=  (/)  /\  B  =  U. B ) )
96, 7, 83bitr4g 280 1  |-  ( A  =  B  ->  ( Lim  A  <->  Lim  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936    = wceq 1649    =/= wne 2552   (/)c0 3573   U.cuni 3959   Ord word 4523   Lim wlim 4525
This theorem is referenced by:  limuni2  4585  0ellim  4586  limuni3  4774  tfinds2  4785  dfom2  4789  limomss  4792  nnlim  4800  limom  4802  ssnlim  4805  onfununi  6541  tfr1a  6593  tz7.44lem1  6601  tz7.44-2  6603  tz7.44-3  6604  oeeulem  6782  limensuc  7222  elom3  7538  r1funlim  7627  rankxplim2  7739  rankxplim3  7740  rankxpsuc  7741  infxpenlem  7830  alephislim  7899  cflim2  8078  winalim  8505  rankcf  8587  gruina  8628  rdgprc0  25176  dfrdg2  25178  dfrdg4  25515  limsucncmpi  25911  limsucncmp  25912
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-in 3272  df-ss 3279  df-uni 3960  df-tr 4246  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-lim 4529
  Copyright terms: Public domain W3C validator