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

Theorem limeq 5922
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 (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Proof of Theorem limeq
StepHypRef Expression
1 ordeq 5917 . . 3 (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2 neeq1 2999 . . 3 (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3 id 22 . . . 4 (𝐴 = 𝐵𝐴 = 𝐵)
4 unieq 4604 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
53, 4eqeq12d 2780 . . 3 (𝐴 = 𝐵 → (𝐴 = 𝐴𝐵 = 𝐵))
61, 2, 53anbi123d 1560 . 2 (𝐴 = 𝐵 → ((Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴) ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵)))
7 df-lim 5915 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
8 df-lim 5915 . 2 (Lim 𝐵 ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵))
96, 7, 83bitr4g 305 1 (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1107   = wceq 1652  wne 2937  c0 4081   cuni 4596  Ord word 5909  Lim wlim 5911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-in 3741  df-ss 3748  df-uni 4597  df-tr 4914  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-ord 5913  df-lim 5915
This theorem is referenced by:  limuni2  5971  0ellim  5972  limuni3  7254  tfinds2  7265  dfom2  7269  limomss  7272  nnlim  7280  limom  7282  ssnlim  7285  onfununi  7646  tfr1a  7698  tz7.44lem1  7709  tz7.44-2  7711  tz7.44-3  7712  oeeulem  7890  limensuc  8348  elom3  8764  r1funlim  8848  rankxplim2  8962  rankxplim3  8963  rankxpsuc  8964  infxpenlem  9091  alephislim  9161  cflim2  9342  winalim  9774  rankcf  9856  gruina  9897  rdgprc0  32163  dfrdg2  32165  dfrdg4  32523  limsucncmpi  32904  limsucncmp  32905
  Copyright terms: Public domain W3C validator