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

Theorem limeq 6206
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 6201 . . 3 (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2 neeq1 3081 . . 3 (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3 id 22 . . . 4 (𝐴 = 𝐵𝐴 = 𝐵)
4 unieq 4852 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
53, 4eqeq12d 2840 . . 3 (𝐴 = 𝐵 → (𝐴 = 𝐴𝐵 = 𝐵))
61, 2, 53anbi123d 1432 . 2 (𝐴 = 𝐵 → ((Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴) ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵)))
7 df-lim 6199 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
8 df-lim 6199 . 2 (Lim 𝐵 ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵))
96, 7, 83bitr4g 316 1 (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  w3a 1083   = wceq 1536  wne 3019  c0 4294   cuni 4841  Ord word 6193  Lim wlim 6195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-v 3499  df-in 3946  df-ss 3955  df-uni 4842  df-tr 5176  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-ord 6197  df-lim 6199
This theorem is referenced by:  limuni2  6255  0ellim  6256  limuni3  7570  tfinds2  7581  dfom2  7585  limomss  7588  nnlim  7596  limom  7598  ssnlim  7602  onfununi  7981  tfr1a  8033  tz7.44lem1  8044  tz7.44-2  8046  tz7.44-3  8047  oeeulem  8230  limensuc  8697  elom3  9114  r1funlim  9198  rankxplim2  9312  rankxplim3  9313  rankxpsuc  9314  infxpenlem  9442  alephislim  9512  cflim2  9688  winalim  10120  rankcf  10202  gruina  10243  rdgprc0  33042  dfrdg2  33044  dfrdg4  33416  limsucncmpi  33797  limsucncmp  33798  dfsucon  39895
  Copyright terms: Public domain W3C validator