Theorem limeq 6178

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 6173	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2996	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4804	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2754	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1437	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6171	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6171	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1088   = wceq 1542   ≠ wne 2934  ∅c0 4209  ∪ cuni 4793  Ord word 6165  Lim wlim 6167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-ral 3058  df-v 3399  df-in 3848  df-ss 3858  df-uni 4794  df-tr 5134  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6169  df-lim 6171

This theorem is referenced by:  limuni2  6227  0ellim  6228  limuni3  7580  tfinds2  7591  dfom2  7595  limomss  7598  nnlim  7606  limom  7608  ssnlim  7612  onfununi  8000  tfr1a  8052  tz7.44lem1  8063  tz7.44-2  8065  tz7.44-3  8066  oeeulem  8251  limensuc  8737  elom3  9177  r1funlim  9261  rankxplim2  9375  rankxplim3  9376  rankxpsuc  9377  infxpenlem  9506  alephislim  9576  cflim2  9756  winalim  10188  rankcf  10270  gruina  10311  rdgprc0  33333  dfrdg2  33335  scutbdaybnd2lim  33644  dfrdg4  33883  limsucncmpi  34264  limsucncmp  34265  dfsucon  40668