Theorem limeq 6374

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 6369	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3004	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4919	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2749	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1437	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6367	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6367	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088   = wceq 1542   ≠ wne 2941  ∅c0 4322  ∪ cuni 4908  Ord word 6361  Lim wlim 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-v 3477  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6365  df-lim 6367

This theorem is referenced by:  limuni2  6424  0ellim  6425  limuni3  7838  tfinds2  7850  dfom2  7854  limomss  7857  nnlim  7866  limom  7868  ssnlim  7872  onfununi  8338  tfr1a  8391  tz7.44lem1  8402  tz7.44-2  8404  tz7.44-3  8405  1ellim  8495  2ellim  8496  oeeulem  8598  limensuc  9151  elom3  9640  r1funlim  9758  rankxplim2  9872  rankxplim3  9873  rankxpsuc  9874  infxpenlem  10005  alephislim  10075  cflim2  10255  winalim  10687  rankcf  10769  gruina  10810  scutbdaybnd2lim  27308  rdgprc0  34754  dfrdg2  34756  dfrdg4  34912  limsucncmpi  35319  limsucncmp  35320  omlimcl2  41977  onexlimgt  41978  onov0suclim  42010  succlg  42064  dflim5  42065  nlim1NEW  42179  nlim2NEW  42180  nlim3  42181  nlim4  42182  dfsucon  42260