Theorem limuni 6311

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2942  ∅c0 4253  ∪ cuni 4836  Ord word 6250  Lim wlim 6252

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 206  df-an 396  df-3an 1087  df-lim 6256

This theorem is referenced by:  limuni2  6312  unizlim  6368  nlimsucg  7664  oa0r  8330  om1r  8336  oarec  8355  oeworde  8386  oeeulem  8394  infeq5i  9324  r1sdom  9463  rankxplim3  9570  cflm  9937  coflim  9948  cflim2  9950  cfss  9952  cfslbn  9954  limsucncmpi  34561  dfom6  41036