Theorem limeq 6400

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 6395	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3021	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4883	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2779	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1465	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6393	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6393	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1570   ≠ wne 2959  ∅c0 4281  ∪ cuni 4872  Ord word 6387  Lim wlim 6389

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6391  df-lim 6393

This theorem is used by:  limuni2  6452  limuni3  7897  tfinds2  7909  dfom2  7913  limomss  7916  nnlim  7925  limom  7927  ssnlim  7931  onfununi  8387  tfr1a  8440  tz7.44lem1  8451  tz7.44-2  8453  tz7.44-3  8454  1ellim  8544  2ellim  8545  oeeulem  8648  limensuc  9211  elom3  9686  r1funlimOLD  9807  r1dmlim  9809  rankxplim2  9934  rankxplim3  9935  rankxpsuc  9936  infxpenlem  10131  alephislim  10201  cflim2  10380  winalim  10819  rankcf  10901  gruina  10942  cutbdaybnd2lim  28240  rdgprc0  36770  dfrdg2  36772  dfrdg4  36930  limsucncmpi  37448  limsucncmp  37449  omlimcl2  44505  onexlimgt  44506  onov0suclim  44537  succlg  44591  dflim5  44592  nlim1NEW  44704  nlim2NEW  44705  nlim3  44706  nlim4  44707  dfsucon  44785