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

Theorem limeq 5699
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 5694 . . 3 (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2 neeq1 2852 . . 3 (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3 id 22 . . . 4 (𝐴 = 𝐵𝐴 = 𝐵)
4 unieq 4415 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
53, 4eqeq12d 2636 . . 3 (𝐴 = 𝐵 → (𝐴 = 𝐴𝐵 = 𝐵))
61, 2, 53anbi123d 1396 . 2 (𝐴 = 𝐵 → ((Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴) ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵)))
7 df-lim 5692 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
8 df-lim 5692 . 2 (Lim 𝐵 ↔ (Ord 𝐵𝐵 ≠ ∅ ∧ 𝐵 = 𝐵))
96, 7, 83bitr4g 303 1 (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036   = wceq 1480  wne 2790  c0 3896   cuni 4407  Ord word 5686  Lim wlim 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-in 3566  df-ss 3573  df-uni 4408  df-tr 4718  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5690  df-lim 5692
This theorem is referenced by:  limuni2  5750  0ellim  5751  limuni3  7006  tfinds2  7017  dfom2  7021  limomss  7024  nnlim  7032  limom  7034  ssnlim  7037  onfununi  7390  tfr1a  7442  tz7.44lem1  7453  tz7.44-2  7455  tz7.44-3  7456  oeeulem  7633  limensuc  8089  elom3  8497  r1funlim  8581  rankxplim2  8695  rankxplim3  8696  rankxpsuc  8697  infxpenlem  8788  alephislim  8858  cflim2  9037  winalim  9469  rankcf  9551  gruina  9592  rdgprc0  31435  dfrdg2  31437  dfrdg4  31735  limsucncmpi  32121  limsucncmp  32122
  Copyright terms: Public domain W3C validator