Theorem limuni 6253

Description: A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)

Assertion

Ref	Expression
limuni	⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Proof of Theorem limuni

Step	Hyp	Ref	Expression
1		df-lim 6198	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1143	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3018  ∅c0 4293  ∪ cuni 4840  Ord word 6192  Lim wlim 6194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-lim 6198

This theorem is referenced by:  limuni2  6254  unizlim  6309  nlimsucg  7559  oa0r  8165  om1r  8171  oarec  8190  oeworde  8221  oeeulem  8229  infeq5i  9101  r1sdom  9205  rankxplim3  9312  cflm  9674  coflim  9685  cflim2  9687  cfss  9689  cfslbn  9691  limsucncmpi  33795  dfom6  39905