Theorem limuni 6251

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 6196	. 2 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))
2	1	simp3bi 1143	1 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3016  ∅c0 4291  ∪ cuni 4838  Ord word 6190  Lim wlim 6192

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 6196

This theorem is referenced by:  limuni2  6252  unizlim  6307  nlimsucg  7557  oa0r  8163  om1r  8169  oarec  8188  oeworde  8219  oeeulem  8227  infeq5i  9099  r1sdom  9203  rankxplim3  9310  cflm  9672  coflim  9683  cflim2  9685  cfss  9687  cfslbn  9689  limsucncmpi  33793  dfom6  39918