Theorem limeq 6329

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

Step	Hyp	Ref	Expression
1		ordeq 6324	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2994	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4874	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2752	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1438	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6322	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6322	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   = wceq 1541   ≠ wne 2932  ∅c0 4285  ∪ cuni 4863  Ord word 6316  Lim wlim 6318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-lim 6322

This theorem is referenced by:  limuni2  6380  limuni3  7794  tfinds2  7806  dfom2  7810  limomss  7813  nnlim  7822  limom  7824  ssnlim  7828  onfununi  8273  tfr1a  8325  tz7.44lem1  8336  tz7.44-2  8338  tz7.44-3  8339  1ellim  8425  2ellim  8426  oeeulem  8529  limensuc  9082  elom3  9557  r1funlim  9678  rankxplim2  9792  rankxplim3  9793  rankxpsuc  9794  infxpenlem  9923  alephislim  9993  cflim2  10173  winalim  10606  rankcf  10688  gruina  10729  cutbdaybnd2lim  27793  rdgprc0  35985  dfrdg2  35987  dfrdg4  36145  limsucncmpi  36639  limsucncmp  36640  omlimcl2  43484  onexlimgt  43485  onov0suclim  43516  succlg  43570  dflim5  43571  nlim1NEW  43683  nlim2NEW  43684  nlim3  43685  nlim4  43686  dfsucon  43764