Theorem limuni 5946

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

Syntax hints:   → wi 4   = wceq 1632   ≠ wne 2932  ∅c0 4058  ∪ cuni 4588  Ord word 5883  Lim wlim 5885

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 385  df-3an 1074  df-lim 5889

This theorem is referenced by:  limuni2  5947  unizlim  6005  nlimsucg  7208  oa0r  7789  om1r  7794  oarec  7813  oeworde  7844  oeeulem  7852  infeq5i  8708  r1sdom  8812  rankxplim3  8919  cflm  9284  coflim  9295  cflim2  9297  cfss  9299  cfslbn  9301  limsucncmpi  32771