Theorem limuni 5785

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

Syntax hints:   → wi 4   = wceq 1483   ≠ wne 2794  ∅c0 3915  ∪ cuni 4436  Ord word 5722  Lim wlim 5724

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 197  df-an 386  df-3an 1039  df-lim 5728

This theorem is referenced by:  limuni2  5786  unizlim  5844  nlimsucg  7042  oa0r  7618  om1r  7623  oarec  7642  oeworde  7673  oeeulem  7681  infeq5i  8533  r1sdom  8637  rankxplim3  8744  cflm  9072  coflim  9083  cflim2  9085  cfss  9087  cfslbn  9089  limsucncmpi  32444