Theorem limeq 6347

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 6342	. . 3 ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
2		neeq1 2988	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
3		id 22	. . . 4 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
4		unieq 4885	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
5	3, 4	eqeq12d 2746	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = ∪ 𝐴 ↔ 𝐵 = ∪ 𝐵))
6	1, 2, 5	3anbi123d 1438	. 2 ⊢ (𝐴 = 𝐵 → ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵)))
7		df-lim 6340	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
8		df-lim 6340	. 2 ⊢ (Lim 𝐵 ↔ (Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086   = wceq 1540   ≠ wne 2926  ∅c0 4299  ∪ cuni 4874  Ord word 6334  Lim wlim 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-lim 6340

This theorem is referenced by:  limuni2  6398  limuni3  7831  tfinds2  7843  dfom2  7847  limomss  7850  nnlim  7859  limom  7861  ssnlim  7865  onfununi  8313  tfr1a  8365  tz7.44lem1  8376  tz7.44-2  8378  tz7.44-3  8379  1ellim  8465  2ellim  8466  oeeulem  8568  limensuc  9124  elom3  9608  r1funlim  9726  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  infxpenlem  9973  alephislim  10043  cflim2  10223  winalim  10655  rankcf  10737  gruina  10778  scutbdaybnd2lim  27736  rdgprc0  35788  dfrdg2  35790  dfrdg4  35946  limsucncmpi  36440  limsucncmp  36441  omlimcl2  43238  onexlimgt  43239  onov0suclim  43270  succlg  43324  dflim5  43325  nlim1NEW  43438  nlim2NEW  43439  nlim3  43440  nlim4  43441  dfsucon  43519