Theorem limeq 6361

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 6356	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 3022	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 23	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4878	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2781	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1460	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6354	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6354	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101   = wceq 1563   ≠ wne 2960  ∅c0 4288  ∪ cuni 4867  Ord word 6348  Lim wlim 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-v 3459  df-ss 3924  df-uni 4868  df-tr 5212  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6352  df-lim 6354

This theorem is referenced by:  limuni2  6413  limuni3  7836  tfinds2  7848  dfom2  7852  limomss  7855  nnlim  7864  limom  7866  ssnlim  7870  onfununi  8316  tfr1a  8369  tz7.44lem1  8380  tz7.44-2  8382  tz7.44-3  8383  1ellim  8471  2ellim  8472  oeeulem  8575  limensuc  9130  elom3  9605  r1funlim  9726  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  infxpenlem  9985  alephislim  10055  cflim2  10235  winalim  10668  rankcf  10750  gruina  10791  cutbdaybnd2lim  27944  rdgprc0  36149  dfrdg2  36151  dfrdg4  36309  limsucncmpi  36813  limsucncmp  36814  omlimcl2  43826  onexlimgt  43827  onov0suclim  43858  succlg  43912  dflim5  43913  nlim1NEW  44025  nlim2NEW  44026  nlim3  44027  nlim4  44028  dfsucon  44106