Theorem limuni 6326

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2943  ∅c0 4256  ∪ cuni 4839  Ord word 6265  Lim wlim 6267

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 397  df-3an 1088  df-lim 6271

This theorem is referenced by:  limuni2  6327  unizlim  6383  nlimsucg  7689  oa0r  8368  om1r  8374  oarec  8393  oeworde  8424  oeeulem  8432  infeq5i  9394  r1sdom  9532  rankxplim3  9639  cflm  10006  coflim  10017  cflim2  10019  cfss  10021  cfslbn  10023  limsucncmpi  34634  dfom6  41138