Theorem limuni 6232

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2934  ∅c0 4211  ∪ cuni 4796  Ord word 6171  Lim wlim 6173

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 210  df-an 400  df-3an 1090  df-lim 6177

This theorem is referenced by:  limuni2  6233  unizlim  6289  nlimsucg  7576  oa0r  8194  om1r  8200  oarec  8219  oeworde  8250  oeeulem  8258  infeq5i  9172  r1sdom  9276  rankxplim3  9383  cflm  9750  coflim  9761  cflim2  9763  cfss  9765  cfslbn  9767  limsucncmpi  34272  dfom6  40692