Theorem limeq 6375

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 6370	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2998	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4914	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2743	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1433	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6368	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6368	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085   = wceq 1534   ≠ wne 2935  ∅c0 4318  ∪ cuni 4903  Ord word 6362  Lim wlim 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-ral 3057  df-v 3471  df-in 3951  df-ss 3961  df-uni 4904  df-tr 5260  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6366  df-lim 6368

This theorem is referenced by:  limuni2  6425  0ellim  6426  limuni3  7850  tfinds2  7862  dfom2  7866  limomss  7869  nnlim  7878  limom  7880  ssnlim  7884  onfununi  8355  tfr1a  8408  tz7.44lem1  8419  tz7.44-2  8421  tz7.44-3  8422  1ellim  8512  2ellim  8513  oeeulem  8615  limensuc  9170  elom3  9663  r1funlim  9781  rankxplim2  9895  rankxplim3  9896  rankxpsuc  9897  infxpenlem  10028  alephislim  10098  cflim2  10278  winalim  10710  rankcf  10792  gruina  10833  scutbdaybnd2lim  27737  rdgprc0  35325  dfrdg2  35327  dfrdg4  35483  limsucncmpi  35865  limsucncmp  35866  omlimcl2  42593  onexlimgt  42594  onov0suclim  42626  succlg  42680  dflim5  42681  nlim1NEW  42795  nlim2NEW  42796  nlim3  42797  nlim4  42798  dfsucon  42876